∀C:ordered_set.
∀a:sequence (os_l C).∀s:segment C.∀H:∀i:nat.a i ∈ s.
∀x:C.∀p:order_converge C a x.
- ∀j. 𝕝_s ≤ (pi1exT23 ???? p j).
+ ∀j. 𝕝_ s ≤ (pi1exT23 ???? p j).
intros; cases p (xi yi Ux Dy Hxy); clear p; simplify;
cases Ux (Ixi Sxi); clear Ux; cases Dy (Dyi Iyi); clear Dy;
cases (Hxy j) (Ia Sa); clear Hxy; cases Ia (Da SSa); cases Sa (Inca SIa); clear Ia Sa;
-intro H2; cases (SSa 𝕝_s H2) (w Hw); simplify in Hw;
+intro H2; cases (SSa 𝕝_ s H2) (w Hw); simplify in Hw;
lapply (H (w+j)) as K; cases (cases_in_segment ? s ? K); apply H3; apply Hw;
qed.
∀C:ordered_set.
∀a:sequence (os_l C).∀s:segment C.∀H:∀i:nat.a i ∈ s.
∀x:C.∀p:order_converge C a x.
- ∀j. (pi2exT23 ???? p j) ≤ 𝕦_s.
+ ∀j. (pi2exT23 ???? p j) ≤ 𝕦_ s.
intros; cases p (xi yi Ux Dy Hxy); clear p; simplify;
cases Ux (Ixi Sxi); clear Ux; cases Dy (Dyi Iyi); clear Dy;
cases (Hxy j) (Ia Sa); clear Hxy; cases Ia (Da SSa); cases Sa (Inca SIa); clear Ia Sa;
-intro H2; cases (SIa 𝕦_s H2) (w Hw); lapply (H (w+j)) as K;
+intro H2; cases (SIa 𝕦_ s H2) (w Hw); lapply (H (w+j)) as K;
cases (cases_in_segment ? s ? K); apply H1; apply Hw;
qed.
cut (∀i.xi i ∈ s) as Hxi; [2:
intros; apply (prove_in_segment (os_l C)); [apply (H3 i)] cases (Hxy i) (H5 _); cases H5 (H7 _);
lapply (H7 0) as K; cases (cases_in_segment ? s ? (H1 i)) (Pl Pu);
- simplify in K:(? ? % ?); apply (hle_transitive (os_l C) (xi i) (a i) 𝕦_s K Pu);] clear H3;
+ simplify in K:(? ? % ?); apply (hle_transitive (os_l C) (xi i) (a i) 𝕦_ s K Pu);] clear H3;
cut (∀i.yi i ∈ s) as Hyi; [2:
intros; apply (prove_in_segment (os_l C)); [2:apply (H2 i)] cases (Hxy i) (_ H5); cases H5 (H7 _);
lapply (H7 0) as K; cases (cases_in_segment ? s ? (H1 i)) (Pl Pu); simplify in K;
- apply (le_transitive 𝕝_s ? ? ? K);apply Pl;] clear H2;
+ apply (le_transitive 𝕝_ s ? ? ? K);apply Pl;] clear H2;
split;
[1: apply (uparrow_to_in_segment s ? Hxi ? Hx);
|2: intros 3 (h);
cut (∀i.xi i ∈ s) as Hxi; [2:
intros; apply (prove_in_segment (os_l C)); [apply (H3 i)] cases (Hxy i) (H5 _); cases H5 (H7 _);
lapply (H7 0) as K; cases (cases_in_segment ? s ? (H1 i)) (Pl Pu);
- simplify in K:(? ? % ?); apply (hle_transitive (os_l C) (xi i) (a i) 𝕦_s K Pu);] clear H3;
+ simplify in K:(? ? % ?); apply (hle_transitive (os_l C) (xi i) (a i) 𝕦_ s K Pu);] clear H3;
cut (∀i.yi i ∈ s) as Hyi; [2:
intros; apply (prove_in_segment (os_l C)); [2:apply (H2 i)] cases (Hxy i) (_ H5); cases H5 (H7 _);
lapply (H7 0) as K; cases (cases_in_segment ? s ? (H1 i)) (Pl Pu); simplify in K;
- apply (le_transitive 𝕝_s ? ? ? K);apply Pl;] clear H2;
+ apply (le_transitive 𝕝_ s ? ? ? K);apply Pl;] clear H2;
letin Xi ≝ (⌊n,≪xi n, Hxi n≫⌋);
letin Yi ≝ (⌊n,≪yi n, Hyi n≫⌋);
cases (restrict_uniform_convergence_uparrow ? S ? (H s) Xi x Hx);