proposition: Lemma extension_approximation_diff_bound: forall x:SubspaceTopology F, -2/3 <= f0 x - extension_approximation (subspace_inc F x) <= 2/3.
proof: Proof. intros. unfold extension_approximation. destruct Urysohns_lemma_function as [g [? [? []]]]. simpl. destruct (f0_bound x). destruct (Rle_or_lt (f0 x) (-1/3)). - replace (g (subspace_inc F x)) with 0. { lra. } symmetry. apply e. econstructor; trivial. now constructor. - destruct (Rle_or_lt (1/3) (f0 x)). + replace (g (subspace_inc F x)) with 1. { lra. } symmetry. apply e0. econstructor; trivial. constructor. lra. + destruct (a (subspace_inc F x)). lra. Qed.
imports: RTopology SeparatednessAxioms RFuncContinuity UniformTopology ContinuousFactorization Coq(Description Max Psatz ClassicalChoice) ZornsLemma(Proj1SigInjective) UrysohnsLemma