proposition: Lemma extension_approximation_continuous: continuous extension_approximation.
proof: Proof. unfold extension_approximation. destruct Urysohns_lemma_function as [g [? [? []]]]. simpl. apply pointwise_continuity. intros. apply sum_continuous. - apply continuous_func_continuous_everywhere, continuous_constant. - now apply const_multiple_continuous, continuous_func_continuous_everywhere. Qed.
imports: RTopology SeparatednessAxioms RFuncContinuity UniformTopology ContinuousFactorization Coq(Description Max Psatz ClassicalChoice) ZornsLemma(Proj1SigInjective) UrysohnsLemma