proposition: Lemma flat_prf : forall (a b : Qpos) (Hab : (a < b)%Q) (f : (XpowM CR 1) -> CR) (Hf : Bcont 1 CR f), {m | is_UniformlyContinuousFunction (flat_raw a b Hab f Hf) m}.
proof: Proof. intros a0 b0 Ha0b0 f Hf. unfold Bcont in Hf. set (IRasCR (inj_Q IR a0)). set (IRasCR (inj_Q IR b0)). assert ({g : XpowM (SubMS CR (fun x : CR => sq (cof_less s x and cof_less x s0))) 1 -> CR | (forall x : XpowM (SubMS CR (fun x : CR => sq (cof_less s x and cof_less x s0))) 1, f (unres 1 (fun x0 : CR => sq (cof_less s x0 and cof_less x0 s0)) x) [=] g x)}). exists (fun x : XpowM (SubMS CR (fun x : CR => sq (cof_less s x and cof_less x s0))) 1 => f (unres 1 (fun x0 : CR => sq (cof_less s x0 and cof_less x0 s0)) x)). intro x; reflexivity. inversion X. assert (cof_less s s0). unfold s. unfold s0. Admitted. Definition flat (a b : Qpos) (Hab : (a < b)%Q) (f : (XpowM CR 1) -> CR) (Hf : Bcont 1 CR f) : UniformlyContinuousSpace Q_as_MetricSpace CR. intros a0 b0 Ha0b0 f Hf. set (flat_prf a0 b0 Ha0b0 f Hf). 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