proposition: Lemma locatedsub_totallybounded_imp_totallyboundedsub : forall (X : CPsMetricSpace) (P : X -> CProp), SubPsMetricSpace P -> located' P -> MStotally_bounded X -> MStotally_bounded (SubPsMetricSpace P).
proof: Proof. intros X P y H0. unfold MStotally_bounded in |- *. intros H1 n. elim (H1 (3 * n + 2)). intros l H2. unfold located' in H0. simpl in |- *. exists (map (Flocfun X P H0 y (3 * n + 2)) l). simpl in |- *. intro x. elim (H2 (from_SubPsMetricSpace X P x)). intros xj xjl H3. exists (Flocfun X P H0 y (n + (n + (n + 0)) + 2) xj). apply map_member with (f := Flocfun X P H0 y (n + (n + (n + 0)) + 2)). exact xjl. unfold Flocfun in |- *. unfold sigT_rec in |- *. unfold sigT_rect in |- *. case Floc. intros. elim s. intros x2 p0 q. generalize H3. case x. intros xn Pn H4. apply leEq_transitive with ((xn[-d]xj)[+](xj[-d]from_SubPsMetricSpace X P x0)). case x0. intros. simpl in |- *. apply ax_d_tri_ineq. apply CPsMetricSpace_is_CPsMetricSpace. astepr (one_div_succ (R:=IR) (n + (n + (n + 0)) + 2)[+] (one_div_succ (n + (n + (n + 0)) + 2)[+] one_div_succ (n + (n + (n + 0)) + 2))). apply plus_resp_leEq_both. apply H4. apply leEq_transitive with (x2[+]one_div_succ (n + (n + (n + 0)) + 2)). apply leEq_transitive with (xj[-d]from_SubPsMetricSpace X P x0). apply eq_imp_leEq. apply csbf_wd_unfolded. intuition. intuition. exact q. apply plus_resp_leEq. apply leEq_transitive with (from_SubPsMetricSpace X P x[-d]xj). unfold set_glb_IR in p0. elim p0. intros. apply a. unfold SubPsMetricSpace in |- *. simpl in |- *. exists x. apply ax_d_com. apply CPsMetricSpace_is_CPsMetricSpace. apply H3. astepr ([1][*]one_div_succ (R:=IR) n). astepr (((Three:IR)[/] Three:IR[//]three_ap_zero IR)[*]one_div_succ n). astepl (one_div_succ (n + (n + (n + 0)) + 2)[+] (Two:IR)[*]one_div_succ (n + (n + (n + 0)) + 2)). astepl (OneR[*]one_div_succ (n + (n + (n + 0)) + 2)[+] (Two:IR)[*]one_div_succ (n + (n + (n + 0)) + 2)). astepl ((OneR[+]Two)[*]one_div_succ (n + (n + (n + 0)) + 2)). stepl ((Three:IR)[*]one_div_succ (n + (n + (n + 0)) + 2)). 2: apply mult_wdl. 2: rational. astepr ((Three:IR)[*]([1][/] Three[//]three_ap_zero IR)[*]one_div_succ n). astepr ((Three:IR)[*](([1][/] Three[//]three_ap_zero IR)[*]one_div_succ n)). apply mult_wdr. unfold one_div_succ in |- *. unfold Snring in |- *. simpl in |- *. astepr (OneR[/] (Three:IR)[*](nring n[+][1])[//] mult_resp_ap_zero IR Three (nring n[+][1]) (three_ap_zero IR) (nringS_ap_zero IR n)). apply eq_div. apply mult_wdr. astepl (Three[*]nring (R:=IR) n[+]Three[*][1]). simpl in |- *. astepr (nring (R:=IR) (n + (n + (n + 0)))[+]Two[+][1]). astepr (nring (R:=IR) n[+]nring (n + (n + 0))[+]Two[+][1]). astepr (nring (R:=IR) n[+](nring n[+]nring (n + 0))[+]Two[+][1]). 3: apply mult_wdl. 3: rational. 2: simpl in |- *. 2: rational. astepr (nring (R:=IR) n[+](nring n[+]nring (n + 0))[+]Two[+][1]). astepr (nring (R:=IR) n[+](nring n[+]nring (n + 0))[+](Two[+][1])). astepl ((ZeroR[+][1][+][1][+][1])[*]nring n[+]([0][+][1][+][1][+][1])). simpl in |- *. astepl (ZeroR[+][1][+][1][+][1][+]([0][+][1][+][1][+][1])[*]nring n). astepr (ZeroR[+][1][+][1][+][1][+](nring n[+](nring n[+]nring (n + 0)))). apply plus_resp_eq. astepr (nring (R:=IR) n[+](nring n[+](nring n[+]nring 0))). simpl in |- *. rational. Qed.
imports: CoRN.metrics.Prod_Sub