proposition: Lemma Tietze_extension_func_continuous: continuous Tietze_extension_func.
proof: Proof. unfold Tietze_extension_func; destruct constructive_definite_description as [g]; simpl. apply net_limit_in_closure with (S:=fun h:UniformTopology R_metric (fun _:X => 0) R_metric_is_metric X_nonempty => continuous (proj1_sig h) (Y:=MetricTopology R_metric R_metric_is_metric)) in n. - rewrite closure_fixes_closed in n. + unfold In in n. now apply <- convert_continuity. + apply continuous_functions_closed_in_uniform_metric. - red. intros. exists i. split. + constructor. + red. unfold convert_approx_to_uniform_space. simpl. destruct extension_approximation_seq as [h [? []]]. simpl. now apply -> convert_continuity. Qed.
imports: RTopology SeparatednessAxioms RFuncContinuity UniformTopology ContinuousFactorization Coq(Description Max Psatz ClassicalChoice) ZornsLemma(Proj1SigInjective) UrysohnsLemma