definition property_sigma ≝
λC:ordered_uniform_space.
∀U.us_unifbase ? U →
- ∃V:sequence (C square → Prop).
+ ∃V:sequence (C squareB → Prop).
(∀i.us_unifbase ? (V i)) ∧
∀a:sequence C.∀x:C.(a ↑ x ∨ a ↓ x) →
(∀n.∀i,j.n ≤ i → n ≤ j → V n 〈a i,a j〉) → U 〈a 0,x〉.
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.
-
+
(* 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".
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
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);]]
+ [ left; apply (selection_uparrow ? Hm a l H4);
+ | right; apply (selection_downarrow ? Hm a l H4);]]
lapply (H9 ?? H10) as H11; [
exists [apply (m 0:nat)] intros;
cases H1;
[cases H5; cases H7; apply (ous_convex ?? H3 ? H11 (H12 (m O)));
|cases H5; cases H7; cases (us_phi4 ?? H3 〈(a (m O)),l〉);
lapply (H14 H11) as H11'; apply (ous_convex ?? H3 〈l,(a (m O))〉 H11' (H12 (m O)));]
- simplify; repeat split; [1,6:intro X; cases (os_coreflexive ?? X)|*: try apply H12;]
- [1:change with (a (m O) ≤ a i);
- apply (trans_increasing ?? H6); intro; apply (le_to_not_lt ?? H4 H14);
- |2:change with (a i ≤ a (m O));
- apply (trans_decreasing ?? H6); intro; apply (le_to_not_lt ?? H4 H16);]]
+ simplify; repeat split;
+ [1,6: apply (le_reflexive l);
+ |2,5: apply (H12 (\fst (m 0)));
+ |3,8: apply (H12 i);
+ |4:change with (a (m O) ≤ a i);
+ apply (trans_increasing a H6 (\fst (m 0)) i); intro; apply (le_to_not_lt ?? H4 H14);
+ |7:change with (a i ≤ a (m O));
+ apply (trans_decreasing ? H6 (\fst (m 0)) i); intro; apply (le_to_not_lt ?? H4 H16);]]
clear H10; intros (p q r); change with (w p 〈a (m q),a (m r)〉);
generalize in match (refl_eq nat (m p));
generalize in match (m p) in ⊢ (? ? ? % → %); intro X; cases X (w1 H15); clear X;
intros (H16); simplify in H16:(? ? ? %); destruct H16;
apply H15; [3: apply le_n]
-[1: lapply (trans_increasing ?? Hm1 p q) as T; [apply not_lt_to_le; apply T;]
+[1: lapply (trans_increasing ? Hm1 p q) as T; [apply not_lt_to_le; apply T;]
apply (le_to_not_lt p q H4);
-|2: lapply (trans_increasing ?? Hm1 p r) as T; [apply not_lt_to_le; apply T;]
+|2: lapply (trans_increasing ? Hm1 p r) as T; [apply not_lt_to_le; apply T;]
apply (le_to_not_lt p r H5);]
qed.