proposition: Lemma extension_approximation_bound: forall x:X, -1/3 <= extension_approximation x <= 1/3.
proof: Proof. intros. unfold extension_approximation. destruct Urysohns_lemma_function as [g]. simpl. destruct a as [? [? []]]. destruct (H0 x). lra. Qed.
imports: RTopology SeparatednessAxioms RFuncContinuity UniformTopology ContinuousFactorization Coq(Description Max Psatz ClassicalChoice) ZornsLemma(Proj1SigInjective) UrysohnsLemma