proposition: Lemma bounded_functions_closed_in_uniform_metric: closed (fun f:uniform_space d y0 => bounded d (Im Full_set (proj1_sig f))) (X:=UniformTopology d y0 d_metric X_inh).
proof: Proof. apply first_countable_sequence_closed. { apply metrizable_impl_first_countable. apply UniformTopology_metrizable. } intros f f0 Hf0 Hf1. unfold In in Hf0. pose proof (metric_space_net_limit_converse _ _ (MetricTopology_metrized _ _ (uniform_metric_is_metric _ _ _ y0 d_metric X_inh)) nat_DS f f0 Hf1 1 ltac:(lra)) as [N HN]. clear Hf1. specialize (Hf0 N) as [y1 [r Hr]]. exists y1, (r+1). intros y Hy. destruct Hy as [x Hx]; subst. specialize (Hr (proj1_sig (f N) x)) as [HfN]. { apply Im_def; auto. } constructor. specialize (HN N ltac:(reflexivity)). pose proof (uniform_metric_lt _ _ _ _ _ _ _ _ _ HN x). pose proof (triangle_inequality _ d d_metric y1 (proj1_sig (f N) x) (proj1_sig f0 x)). rewrite metric_sym in H; auto. lra. Qed.
imports: MetricSpaces FunctionalExtensionality Completeness Description Max Psatz Lra