proposition: Lemma cdsub'_uni_cont : forall y : M, uni_continuous (cdsub' y).
proof: Proof. intros. unfold uni_continuous. unfold cdsub'. simpl. intros. elim (power_big C Two). intros k H1. 3: apply one_less_two. 2: apply less_leEq; apply constant_positive. exists (n + k). intros. astepl (C[*](dIR (dsub' M P y x) (dsub' M P y y0))). cut (C[*]dIR (dsub' M P y x) (dsub' M P y y0)[<=]C[*](dsub M P x y0)). intros. cut (C[*](dsub M P x y0)[<] nexp IR n ([1][/] Two[//]H)). intros. apply leEq_less_trans with (C[*](dsub M P x y0)); auto with algebra. cut (Two[^]k[*](dsub M P x y0)[<] nexp IR n ([1][/] Two[//]H)). intros. cut (C[*](dsub M P x y0)[<=]Two[^]k[*](dsub M P x y0)). intros. apply leEq_less_trans with (Two[^]k[*](dsub M P x y0)); auto with algebra. apply mult_resp_leEq_rht; auto. apply dsub_nneg. astepr (Two[^]k[*](nexp IR (n + k) ([1][/] Two[//]H))). apply mult_resp_less_lft; auto. apply nexp_resp_pos. cut (([1]:IR)[<]Two). cut ([0][<]([1]:IR)). intros. apply less_transitive_unfolded with ([1]:IR); auto. apply pos_one. apply one_less_two. apply exp_prop. apply dsub'_is_lipschitz. unfold dIR. astepr (ABSIR (C[*](dsub' M P y x[-]dsub' M P y y0))). apply AbsIR_mult. apply less_leEq. apply constant_positive. apply ABSIR_wd; auto with algebra. Qed.
imports: CoRN.metrics.ContFunctions CoRN.metrics.CMetricSpaces CoRN.metrics.CPMSTheory