proposition: Lemma bounded_Tietze_extension_theorem: forall (X:TopologicalSpace) (F:Ensemble X) (f:SubspaceTopology F -> RTop), normal_sep X -> closed F -> continuous f -> (forall x:SubspaceTopology F, -1 <= f x <= 1) -> exists g:X -> RTop, continuous g /\ (forall x:SubspaceTopology F, g (subspace_inc F x) = f x) /\ (forall x:X, -1 <= g x <= 1).
proof: Proof. intros. destruct (classic (inhabited X)) as [Hinh|Hempty]. - destruct (choice (fun (FG:{FG:Ensemble X * Ensemble X | let (F,G):=FG in closed F /\ closed G /\ Intersection F G = Empty_set}) (phi:X -> RTop) => let (F,G):=proj1_sig FG in continuous phi /\ (forall x:X, 0 <= phi x <= 1) /\ (forall x:X, In F x -> phi x = 0) /\ (forall x:X, In G x -> phi x = 1))) as [choice_fun]. + intros. destruct x as [[F' G] [? []]]. now apply UrysohnsLemma. + pose (Urysohns_lemma_function := fun (F G:Ensemble X) (HF:closed F) (HG:closed G) (Hdisj:Intersection F G = Empty_set) => exist (fun (f:X -> RTop) => continuous f /\ (forall x:X, 0 <= f x <= 1) /\ (forall x:X, In F x -> f x = 0) /\ (forall x:X, In G x -> f x = 1)) (choice_fun (exist _ (F,G) (conj HF (conj HG Hdisj)))) (H3 (exist _ (F,G) (conj HF (conj HG Hdisj))))). clearbody Urysohns_lemma_function. clear choice_fun H3. exists (Tietze_extension_func X F H0 f H1 H2 Hinh Urysohns_lemma_function). split. * apply Tietze_extension_func_continuous. * split; intros. ** apply Tietze_extension_func_is_extension. ** apply Tietze_extension_func_bound. - exists (fun x:X => False_rect _ (Hempty (inhabits x))). split. + apply pointwise_continuity. intros. destruct (Hempty (inhabits x)). + split; intros. * destruct x. destruct (Hempty (inhabits x)). * destruct (Hempty (inhabits x)). Qed.
imports: RTopology SeparatednessAxioms RFuncContinuity UniformTopology ContinuousFactorization Coq(Description Max Psatz ClassicalChoice) ZornsLemma(Proj1SigInjective) UrysohnsLemma