(**************************************************************************)
include "ordered_uniform.ma".
-
+include "russell_support.ma".
(* Definition 3.5 *)
alias num (instance 0) = "natural number".
lemma max_le_r: ∀n,m,z.max n m ≤ z → m ≤ z.
intros; rewrite > sym_max in H; apply (max_le_l ??? H);
qed.
-
-definition hide ≝ λT:Type.λx:T.x.
-
-notation < "\blacksquare" non associative with precedence 50 for @{'hide}.
-interpretation "hide" 'hide = (hide _ _).
-interpretation "hide2" 'hide = (hide _ _ _).
-
-definition inject ≝ λP.λa:nat.λp:P a. ex_introT ? P ? p.
-coercion cic:/matita/dama/property_sigma/inject.con 0 1.
-definition eject ≝ λP.λc: ∃n:nat.P n. match c with [ ex_introT w _ ⇒ w].
-coercion cic:/matita/dama/property_sigma/eject.con.
-
+
(* Lemma 3.6 *)
lemma sigma_cauchy:
∀C:ordered_uniform_space.property_sigma C →
∀a:sequence C.∀l:C.(a ↑ l ∨ a ↓ l) → a is_cauchy → a uniform_converges l.
intros 8; cases (H ? H3) (w H5); cases H5 (H8 H9); clear H5;
+alias symbol "pair" = "Pair construction".
+letin spec ≝ (λz,k:nat.∀i,j,l:nat.k ≤ i → k ≤ j → l ≤ z → w l 〈a i,a j〉);
letin m ≝ (hide ? (let rec aux (i:nat) : nat ≝
match i with
[ O ⇒ match H2 (w i) ? with [ ex_introT k _ ⇒ k ]
| S i' ⇒ max (match H2 (w i) ? with [ ex_introT k _ ⇒ k ]) (S (aux i'))
] in aux
- :
- ∀z:nat.∃k:nat.∀i,j,l.k ≤ i → k ≤ j → l ≤ z → w l 〈a i, a j〉));
+ : ∀z.∃k. spec z k)); unfold spec in aux ⊢ %;
[1,2:apply H8;
|3: intros 3; cases (H2 (w n) (H8 n)); simplify in ⊢ (? (? % ?) ?→?);
simplify in ⊢ (?→? (? % ?) ?→?);
intros; lapply (H5 i j) as H14;
[2: apply (max_le_l ??? H6);|3:apply (max_le_l ??? H7);]
cases (le_to_or_lt_eq ?? H10); [2: destruct H11; destruct H4; assumption]
- generalize in match H6; generalize in match H7;
- cases (aux n1); simplify in ⊢ (? (? ? %) ?→? (? ? %) ?→?); intros;
- apply H12; [3: apply le_S_S_to_le; assumption]
+ cases (aux n1) in H6 H7 ⊢ %; simplify in ⊢ (? (? ? %) ?→? (? ? %) ?→?); intros;
+ apply H6; [3: apply le_S_S_to_le; assumption]
apply lt_to_le; apply (max_le_r w1); assumption;
|4: intros; clear H6; rewrite > H4 in H5;
rewrite < (le_n_O_to_eq ? H11); apply H5; assumption;]
-cut (((m : nat→nat) : sequence nat_ordered_set) is_strictly_increasing) as Hm; [2:
+cut ((⌊x,(m x:nat)⌋ : sequence nat_ordered_set) is_strictly_increasing) as Hm; [2:
intro n; change with (S (m n) ≤ m (S n)); unfold m;
whd in ⊢ (? ? %); apply (le_max ? (S (m n)));]
-cut (((m : nat→nat) : sequence nat_ordered_set) is_increasing) as Hm1; [2:
+cut ((⌊x,(m x:nat)⌋ : sequence nat_ordered_set) is_increasing) as Hm1; [2:
intro n; intro L; change in L with (m (S n) < m n);
lapply (Hm n) as L1; change in L1 with (m n < m (S n));
lapply (trans_lt ??? L L1) as L3; apply (not_le_Sn_n ? L3);]
-clearbody m;
-cut ((λx:nat.a (m x))↑ l ∨ (λx:nat.a (m x)) ↓ l) as H10; [2:
+clearbody m; unfold spec in m Hm Hm1; clear spec;
+cut (⌊x,a (m x)⌋ ↑ l ∨ ⌊x,a (m x)⌋ ↓ l) as H10; [2:
cases H1;
[ left; apply (selection_uparrow ?? Hm a l H4);
| right; apply (selection_downarrow ?? Hm a l H4);]]