proposition: Lemma uniform_metric_is_metric: metric uniform_metric.
proof: Proof. constructor; intros. - unfold uniform_metric. destruct x as [f0 Hf]; destruct y as [g0 Hg]. destruct sup. destruct sup. simpl. assert (Im Full_set (fun x:X => d (f0 x) (g0 x)) = Im Full_set (fun x:X => d (g0 x) (f0 x))). { apply Extensionality_Ensembles; split; red; intros. - destruct H. exists x1. + constructor. + rewrite metric_sym; trivial. - destruct H. exists x1. + constructor. + rewrite metric_sym; trivial. } apply Rle_antisym. + apply i. rewrite H. apply i0. + apply i0. rewrite <- H. apply i. - destruct x as [f0 Hf]; destruct y as [g0 Hg]; destruct z as [h0 Hh]. simpl. repeat destruct sup; simpl. apply i. red; intros. destruct H. rewrite H0. apply Rle_trans with (d (f0 x2) (g0 x2) + d (g0 x2) (h0 x2)). + apply d_metric. + assert (d (f0 x2) (g0 x2) <= x0) by (apply i0; exists x2; trivial). assert (d (g0 x2) (h0 x2) <= x1) by (apply i1; exists x2; trivial). auto with real. - destruct x as [f0 Hf]. simpl. destruct sup; simpl. apply Rle_antisym. + apply i. red; intros. destruct H. rewrite metric_zero in H0; trivial. right; trivial. + apply i. destruct X_inhabited as [x0]. exists x0. * constructor. * symmetry; apply d_metric. - destruct x as [f0 Hf]; destruct y as [g0 Hg]. apply ProofIrrelevance.ProofIrrelevanceTheory.subset_eq_compat. extensionality x. apply d_metric. simpl in H. destruct sup in H. simpl in H. subst x0. apply Rle_antisym. + apply i; exists x; trivial. constructor. + cut (d (f0 x) (g0 x) >= 0); auto with real. apply metric_nonneg. assumption. Qed.
imports: MetricSpaces FunctionalExtensionality Completeness Description Max Psatz Lra