proposition: Lemma L0_ext_uc : forall (a b c d : Q) (f : (QsubMS a b) -> CR) (Hab : (a < b)%Q) (Hcd : (c < d)%Q), {m : Qpos -> QposInf | is_UniformlyContinuousFunction (L0_ext_def a b c d Hab Hcd f) m}.
proof: Proof. Admitted. Definition L0 (a b c d : Q) (f : (QsubMS a b) -> CR) (Hab : (a < b)%Q) (Hcd : (c < d)%Q) : UniformlyContinuousSpace Q_as_MetricSpace CR. intros a0 b0 c d f Ha0b0 Hcd. set (L0_ext_uc a0 b0 c d f Ha0b0 Hcd). inversion s. exact (Build_UniformlyContinuousFunction H). Defined.
imports: ssreflect CSetoids CSetoidFun CFields CPolynomials Program Omega Equivalence Morphisms Wf Morphisms CRings CRing_Homomorphisms Rational Setoid CPoly_NthCoeff CPoly_Degree CReals Intervals CauchySeq IntervalFunct MoreIntervals MoreFunctions Composition seq bigopsClass Structures ProductMetric CRIR Integration Qmetric QposMinMax QMinMax iso_CReals