proposition: Lemma Tietze_extension_func_bound: forall x:X, -1 <= Tietze_extension_func x <= 1.
proof: Proof. intros. cut (Rabs (Tietze_extension_func x) <= 1). { intros. unfold Rabs in H. destruct Rcase_abs in H; lra. } unfold Tietze_extension_func. destruct constructive_definite_description as [[g]]. simpl. assert (bound (Im Full_set (fun x:X => R_metric 0 0))). { exists 0. red. intros. destruct H. right. rewrite H0. apply R_metric_is_metric. } apply Rle_trans with (uniform_metric _ _ R_metric_is_metric X_nonempty (exist _ (fun _:X => 0) H) (exist _ g b)). - unfold uniform_metric. simpl. destruct sup. simpl. apply i. exists x. + constructor. + unfold R_metric. f_equal. auto with real. - apply lt_plus_epsilon_le. intros. unshelve refine (let H1:=metric_space_net_limit_converse _ _ _ _ _ _ n eps H0 in _); [ | | clearbody H1 ]; shelve_unifiable. { apply MetricTopology_metrized. } destruct H1 as [N]. refine (Rle_lt_trans _ _ _ (triangle_inequality _ _ _ _ (convert_approx_to_uniform_space N) _) _). { apply uniform_metric_is_metric. } apply Rplus_lt_compat. + apply Rle_lt_trans with (1 - (2/3)^N). * unfold uniform_metric. simpl. destruct sup. simpl. apply i. red. intros. destruct H2. rewrite H3. clear y H3. unfold R_metric. destruct extension_approximation_seq as [h [? []]]. destruct (a x1). simpl. unfold Rabs. destruct Rcase_abs; lra. * assert ((2/3)^N > 0). { apply pow_lt; lra. } lra. + rewrite metric_sym. * apply H1. constructor. * apply uniform_metric_is_metric. Qed.
imports: RTopology SeparatednessAxioms RFuncContinuity UniformTopology ContinuousFactorization Coq(Description Max Psatz ClassicalChoice) ZornsLemma(Proj1SigInjective) UrysohnsLemma