proposition: Lemma lem20 : forall (m : nat) (X : MetricSpace) (Y : MetricSpace) (f : (XpowM CR m) -> X) (g : (XpowM CR m) -> Y) (Hf : Bcont m X f) (Hg : Bcont m Y g), Bcont m (ProductMS X Y) (pairFG m X Y f g).
proof: Proof. intros m X Y f g Hf Hg. unfold Bcont. intros a0 b0 Ha0b0 g0 Hg0. unfold Bcont in Hf. assert ({f' : XpowM (SubMS CR (fun x : CR => sq (cof_less a0 x and cof_less x b0))) m -> X | (forall x : XpowM (SubMS CR (fun x : CR => sq (cof_less a0 x and cof_less x b0))) m, f (unres m (fun x0 : CR => sq (cof_less a0 x0 and cof_less x0 b0)) x) [=] f' x)}). exists (fun x => fst (g0 x)). intro x. unfold pairFG in Hg0. destruct (Hg0 x). rewrite <- H. simpl; reflexivity. inversion X0. elim (Hf a0 b0 Ha0b0 x H). intros mu1 H0. unfold Bcont in Hg. assert ({g' : XpowM (SubMS CR (fun x : CR => sq (cof_less a0 x and cof_less x b0))) m -> Y | (forall x : XpowM (SubMS CR (fun x : CR => sq (cof_less a0 x and cof_less x b0))) m, g (unres m (fun x0 : CR => sq (cof_less a0 x0 and cof_less x0 b0)) x) [=] g' x)}). exists (fun x => snd (g0 x)). intro x0. unfold pairFG in Hg0. destruct (Hg0 x0). rewrite <- H2. simpl; reflexivity. inversion X1. elim (Hg a0 b0 Ha0b0 x0 H1). intros mu2 H2. exists (fun x : Qpos => QposInf_min (mu1 x) (mu2 x)). unfold is_UniformlyContinuousFunction. intros e a1 b1 H3. unfold is_UniformlyContinuousFunction in H0, H2. assert (ball_ex (mu1 e) a1 b1). apply ball_ex_weak_le with (QposInf_min (mu1 e) (mu2 e)). apply QposInf_min_lb_l. exact H3. assert (ball_ex (mu2 e) a1 b1). apply ball_ex_weak_le with (QposInf_min (mu1 e) (mu2 e)). apply QposInf_min_lb_r. exact H3. assert (ball e (x a1) (x b1)). apply H0. exact H4. assert (ball e (x0 a1) (x0 b1)). apply H2. exact H5. simpl; unfold prod_ball; split. destruct (Hg0 a1). rewrite <- H8. destruct (Hg0 b1). rewrite <- H10. simpl. rewrite H. rewrite H. exact H6. simpl. destruct (Hg0 a1). rewrite <- H9. destruct (Hg0 b1). rewrite <- H11. simpl. rewrite H1. rewrite H1. exact H7. Qed.
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