proposition: Lemma continuous_functions_at_point_closed_in_uniform_metric: forall x0:point_set X, closed (fun f:uniform_space d y0 => continuous_at (proj1_sig f) x0 (Y:=MetricTopology d d_metric)) (X:=UniformTopology d y0 d_metric X_inh).
proof: Proof. intros. apply first_countable_sequence_closed. { apply metrizable_impl_first_countable. apply UniformTopology_metrizable. } intros f f0 Hf Hf0. pose proof (MetricTopology_metrized _ d d_metric (proj1_sig f0 x0)) as Hf0_nbhd_basis. apply open_neighborhood_basis_is_neighborhood_basis in Hf0_nbhd_basis. apply continuous_at_neighborhood_basis with (1:=Hf0_nbhd_basis). clear Hf0_nbhd_basis. intros V HV. destruct HV as [r Hr]. assert (r/3>0) as Hr3 by lra. destruct (metric_space_net_limit_converse _ _ (MetricTopology_metrized _ _ (uniform_metric_is_metric X Y d y0 d_metric X_inh)) nat_DS f f0 Hf0 (r/3) Hr3) as [N HN]. assert (neighborhood (inverse_image (proj1_sig (f N)) (open_ball d (proj1_sig (f N) x0) (r/3))) x0) as Hx0_nbhd. { apply Hf. pose proof (MetricTopology_metrized _ d d_metric (proj1_sig (f N) x0)) as Hnbhd. apply open_neighborhood_basis_is_neighborhood_basis in Hnbhd. apply Hnbhd. constructor; trivial. } eapply neighborhood_upward_closed; eauto. clear Hx0_nbhd. intros x [[Hx]]. constructor. constructor. apply Rle_lt_trans with (d (proj1_sig f0 x0) (proj1_sig (f N) x0) + d (proj1_sig (f N) x0) (proj1_sig f0 x)). { apply d_metric. } apply Rle_lt_trans with (d (proj1_sig f0 x0) (proj1_sig (f N) x0) + d (proj1_sig (f N) x0) (proj1_sig (f N) x) + d (proj1_sig (f N) x) (proj1_sig f0 x)). { assert (d (proj1_sig (f N) x0) (proj1_sig f0 x) <= d (proj1_sig (f N) x0) (proj1_sig (f N) x) + d (proj1_sig (f N) x) (proj1_sig f0 x)) by apply d_metric. lra. } rewrite (metric_sym _ d d_metric (proj1_sig (f N) x) (proj1_sig f0 x)). pose proof (uniform_metric_lt X Y d y0 d_metric X_inh f0 (f N) _ (HN N ltac:(reflexivity)) x0). pose proof (uniform_metric_lt X Y d y0 d_metric X_inh f0 (f N) _ (HN N ltac:(reflexivity)) x). lra. Qed.
imports: MetricSpaces FunctionalExtensionality Completeness Description Max Psatz Lra