proposition: Lemma uniform_metric_lt (f g : uniform_space) (r : R) : uniform_metric f g < r -> forall x : X, d (proj1_sig f x) (proj1_sig g x) < r.
proof: Proof. intros Hfg x. destruct f as [f Hf], g as [g Hg]. simpl. unfold uniform_metric in Hfg. destruct sup as [d_fg]. simpl in *. eapply Rle_lt_trans; eauto. clear r Hfg. apply i. exists x; auto with sets. Qed.
imports: MetricSpaces FunctionalExtensionality Completeness Description Max Psatz Lra