proposition: Lemma open_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 (bounded_Tietze_extension_theorem _ F f) as [g0 [? []]]; trivial. { intros. split; left; apply H2. } pose (G := characteristic_function_to_ensemble (fun x:X => g0 x = 1 \/ g0 x = -1)). destruct (UrysohnsLemma _ H G F) as [phi [? [? []]]]; trivial. - replace G with (inverse_image g0 (Union (Singleton 1) (Singleton (-1)))). + red. rewrite <- inverse_image_complement. apply H3. apply (closed_union2 (X:=RTop)); apply Hausdorff_impl_T1_sep; apply T3_sep_impl_Hausdorff; apply normal_sep_impl_T3_sep; apply metrizable_impl_normal_sep; exists R_metric; (apply R_metric_is_metric || apply RTop_metrization). + extensionality_ensembles_inv; constructor. * now left. * now right. * destruct H7; [left | right ]; now rewrite H6. - extensionality_ensembles. assert (-1 < g0 x < 1). { change x with (subspace_inc F (exist _ x H7)). now rewrite H4. } lra. - exists (fun x => phi x * g0 x). split. { apply pointwise_continuity. intros. apply product_continuous; now apply continuous_func_continuous_everywhere. } split. { intros. rewrite H9. - replace (1*g0 (subspace_inc F x)) with (g0 (subspace_inc F x)) by auto with real. apply H4. - now destruct x. } intros. apply and_comm, Rabs_def2. rewrite Rabs_mult. rewrite (Rabs_right (phi x)); [ | apply Rle_ge; apply H7 ]. destruct (classic (In G x)). { rewrite H8; trivial. lra. } assert (Rabs (g0 x) < 1). { assert (Rabs (g0 x) <= 1). { destruct (H5 x). unfold Rabs; destruct Rcase_abs; lra. } destruct H11; trivial. contradiction H10. unfold Rabs in H11. destruct Rcase_abs in H11; constructor. - lra. - now left. } destruct (H7 x). apply Rle_lt_trans with (Rabs (g0 x)); trivial. pattern (Rabs (g0 x)) at 2. replace (Rabs (g0 x)) with (1*Rabs (g0 x)) by auto with real. apply Rmult_le_compat_r; trivial. apply Rabs_pos. Qed.
imports: RTopology SeparatednessAxioms RFuncContinuity UniformTopology ContinuousFactorization Coq(Description Max Psatz ClassicalChoice) ZornsLemma(Proj1SigInjective) UrysohnsLemma