proposition: Lemma Linf_func_metric_space_class : ExtMetricSpaceClass T.
proof: Proof. match goal with | H : NonEmpty X |- _ => destruct H as [x0] end. constructor. + apply func_ball_proper. + intros f g x; apply mspc_inf. + intros e e_neg f g A. specialize (A x0). eapply mspc_negative; eauto. + intros e e_nonneg f x; now apply mspc_refl. + intros e f g A x; now apply mspc_symm. + intros e1 e2 f g h A1 A2 x. now apply mspc_triangle with (b := func g x). + intros e f g A x. apply mspc_closed; intros d A1. now apply A. Qed.
imports: CoRN.algebra.RSetoid CoRN.metric2.Metric CoRN.metric2.UniformContinuity Coq.QArith.QArith MathClasses.theory.setoids MathClasses.theory.products MathClasses.implementations.stdlib_rationals MathClasses.interfaces.abstract_algebra MathClasses.implementations.QType_rationals MathClasses.interfaces.additional_operations CoRN.tactics.Qauto Coq.QArith.QOrderedType MathClasses.theory.rings MathClasses.theory.dec_fields MathClasses.orders.rings MathClasses.orders.dec_fields MathClasses.theory.nat_pow MathClasses.interfaces.naturals MathClasses.interfaces.orders CoRN.reals.fast.CRGeometricSum