proposition: Lemma plus_resp_uni_continuous : forall (X : CPsMetricSpace) (f g : CSetoid_fun X IR_as_CPsMetricSpace) (H : uni_continuous f) (H1 : uni_continuous g), uni_continuous (compose_CSetoid_bin_fun X IR_as_CPsMetricSpace IR_as_CPsMetricSpace f g (csg_op (c:=IR))).
proof: Proof. unfold uni_continuous in |- *. unfold IR_as_CPsMetricSpace in |- *. unfold dIR_as_CSetoid_fun in |- *. unfold dIR in |- *. intros X f g H H0. intros n H1. elim (H (S n) H1). intros x H2. elim (H0 (S n) H1). intros x0 H3. exists (Nat.max x x0). intros x1 y H6. astepl (ABSIR (f x1[-]f y[+](g x1[-]g y))). apply leEq_less_trans with (ABSIR (f x1[-]f y)[+]ABSIR (g x1[-]g y)). apply IR_tri_ineq. apply less_leEq_trans with ((OneR[/] Two:IR[//]H1)[^]S n[+]ABSIR (g x1[-]g y)). apply plus_resp_less_rht. generalize H2. simpl in |- *. intro H7. apply H7. generalize H6. intro H8. apply less_leEq_trans with (nexp IR (Nat.max x x0) ([1][/] [0][+][1][+][1][//]H1)). apply H8. 3: simpl in |- *. astepl (nexp IR (Nat.max x x0) ([1][/] Two:IR[//]H1)). astepr (nexp IR x ([1][/] Two:IR[//]H1)). astepl ((OneR[/] Two:IR[//]H1)[^]Nat.max x x0). astepr ((OneR[/] Two:IR[//]H1)[^]x). apply small_nexp_resp_le. apply shift_leEq_div. apply pos_two. astepl ZeroR. apply less_leEq. apply pos_one. apply shift_div_leEq. apply pos_two. astepr (Two:IR). apply less_leEq. apply one_less_two. intuition. apply leEq_transitive with ((OneR[/] Two:IR[//]H1)[^]S n[+]([1][/] Two:IR[//]H1)[^]S n). apply plus_resp_leEq_lft. apply less_leEq. generalize H3. simpl in |- *. intro H7. apply H7. apply less_leEq_trans with (nexp IR (Nat.max x x0) ([1][/] Two:IR[//]H1)). exact H6. astepr (nexp IR x0 ([1][/] Two:IR[//]H1)). astepl ((OneR[/] Two:IR[//]H1)[^]Nat.max x x0). astepr ((OneR[/] Two:IR[//]H1)[^]x0). apply small_nexp_resp_le. apply shift_leEq_div. apply pos_two. astepl ZeroR. apply less_leEq. apply pos_one. apply shift_div_leEq. apply pos_two. astepr (Two:IR). apply less_leEq. apply one_less_two. intuition. apply eq_imp_leEq. astepl ((Two:IR)[*]([1][/] Two:IR[//]H1)[^]S n). astepl ((Two:IR)[*]([1][^]S n[/] (Two:IR)[^]S n[//]nexp_resp_ap_zero (S n) H1)). astepl ((Two:IR)[*]([1][/] (Two:IR)[^]S n[//]nexp_resp_ap_zero (S n) H1)). astepl ((Two:IR)[*] (([1][/] (Two:IR)[^]n[//]nexp_resp_ap_zero n H1)[*]([1][/] Two:IR[//]H1))). 2: apply mult_wdr. 2: astepl (([1][/] Two:IR[//]H1)[^]S n). 3: astepl (([1][/] Two:IR[//]H1)[^]n[*]([1][/] Two:IR[//]H1)). rstepl (([1][/] (Two:IR)[^]n[//]nexp_resp_ap_zero n H1)[*]Two[*] ([1][/] Two:IR[//]H1)). astepl (([1][/] (Two:IR)[^]n[//]nexp_resp_ap_zero n H1)[*] (Two[*]([1][/] Two:IR[//]H1))). rstepl (([1][/] (Two:IR)[^]n[//]nexp_resp_ap_zero n H1)[*][1]). rstepl ([1][/] (Two:IR)[^]n[//]nexp_resp_ap_zero n H1). astepl ((OneR[/] Two:IR[//]H1)[^]n). apply eq_reflexive. 3: apply AbsIR_wd. 3: rational. astepr ((OneR[/] Two:IR[//]H1)[^]S n). apply eq_reflexive. astepr (([1][/] Two:IR[//]H1)[^]n[*]([1][/] Two:IR[//]H1)). apply eq_reflexive. Qed.
imports: CoRN.metrics.ContFunctions