proposition: Lemma continuous_functions_closed_in_uniform_metric: closed (fun f:uniform_space d y0 => continuous (proj1_sig f) (Y:=MetricTopology d d_metric)) (X:=UniformTopology d y0 d_metric X_inh).
proof: Proof. replace (fun f:uniform_space d y0 => continuous (proj1_sig f) (Y:=MetricTopology d d_metric)) with (IndexedIntersection (fun (x0:point_set X) (f:uniform_space d y0) => continuous_at (proj1_sig f) x0 (Y:=MetricTopology d d_metric))). { apply (@closed_indexed_intersection (UniformTopology d y0 d_metric X_inh)), continuous_functions_at_point_closed_in_uniform_metric. } apply Extensionality_Ensembles; split; intros f ?. - destruct H. now apply pointwise_continuity. - constructor. intros x. unfold In in *. now apply continuous_func_continuous_everywhere. Qed.
imports: MetricSpaces FunctionalExtensionality Completeness Description Max Psatz Lra