proposition: Lemma Tietze_extension_func_is_extension: forall x:SubspaceTopology F, Tietze_extension_func (subspace_inc F x) = f x.
proof: Proof. intros. apply R_metric_is_metric. apply Rle_antisym. 2: { apply Rge_le, metric_nonneg, R_metric_is_metric. } apply lt_plus_epsilon_le; intros. unfold Tietze_extension_func; destruct constructive_definite_description as [[g]]; simpl. assert (eps/2 > 0) by lra. unshelve refine (let H1:=metric_space_net_limit_converse _ _ _ _ _ _ n (eps/2) H0 in _); [ | | clearbody H1 ]; shelve_unifiable. { apply MetricTopology_metrized. } destruct H1 as [N1]. assert (Rabs (2/3) < 1). { rewrite Rabs_right; lra. } destruct (pow_lt_1_zero (2/3) H2 (eps/2) H0) as [N2]. pose (N := Nat.max N1 N2). apply Rle_lt_trans with (R_metric (g (subspace_inc F x)) (proj1_sig (extension_approximation_seq N) (subspace_inc F x)) + R_metric (proj1_sig (extension_approximation_seq N) (subspace_inc F x)) (f x)). { apply triangle_inequality, R_metric_is_metric. } replace (0+eps) with (eps/2+eps/2) by field. apply Rplus_lt_compat. - rewrite metric_sym; try apply R_metric_is_metric. assert (DS_ord N1 N) by apply Nat.le_max_l. apply Rle_lt_trans with (2:=H1 N H4). unfold uniform_metric; simpl; destruct sup; simpl. apply i. exists (subspace_inc F x). { constructor. } apply R_metric_is_metric. - assert ((N >= N2)%nat) by apply Nat.le_max_r. apply Rle_lt_trans with (2:=H3 N H4). rewrite Rabs_right. + destruct extension_approximation_seq as [h [? []]]; simpl. unfold R_metric. destruct (a0 x). unfold Rabs; destruct Rcase_abs; lra. + apply Rle_ge, pow_le; lra. Qed.
imports: RTopology SeparatednessAxioms RFuncContinuity UniformTopology ContinuousFactorization Coq(Description Max Psatz ClassicalChoice) ZornsLemma(Proj1SigInjective) UrysohnsLemma