proposition: Lemma dsub'_uni_continuous'' : forall (X : CPsMetricSpace) (P : X -> CProp) (x : X), uni_continuous'' (dsub'_as_cs_fun P x).
proof: Proof. intros X P x. unfold dsub'_as_cs_fun in |- *. unfold dsub' in |- *. apply uni_continuous'_imp_uni_continuous''. unfold from_SubPsMetricSpace in |- *. unfold uni_continuous' in |- *. simpl in |- *. intro n. exists n. intros x0 x1. case x0. case x1. intros. generalize H. simpl in |- *. intro. apply leEq_transitive with (scs_elem0[-d]scs_elem). 2: exact H0. unfold dIR in |- *. astepl (AbsIR ((scs_elem0[-d]x)[-](scs_elem[-d]x))). astepl (AbsIR ((x[-d]scs_elem0)[-](scs_elem[-d]x))). astepl (AbsIR ((x[-d]scs_elem0)[-](x[-d]scs_elem))). apply AbsSmall_imp_AbsIR. apply rev_tri_ineq. apply csf_wd. apply cg_minus_wd. intuition. apply ax_d_com. apply CPsMetricSpace_is_CPsMetricSpace. apply csf_wd. apply cg_minus_wd. apply ax_d_com. apply CPsMetricSpace_is_CPsMetricSpace. intuition. Qed.
imports: CoRN.metrics.IR_CPMSpace