1 (**************************************************************************)
4 (* ||A|| A project by Andrea Asperti *)
6 (* ||I|| Developers: *)
7 (* ||T|| The HELM team. *)
8 (* ||A|| http://helm.cs.unibo.it *)
10 (* \ / This file is distributed under the terms of the *)
11 (* v GNU General Public License Version 2 *)
13 (**************************************************************************)
15 include "sandwich_corollary.ma".
19 λR.λml:mlattice R.λxn:sequence ml.λx:ml.
20 increasing ? xn → upper_bound ? xn x ∧ xn ⇝ x.
23 λR.λml:mlattice R.λxn:sequence ml.λx:ml.
24 decreasing ? xn → lower_bound ? xn x ∧ xn ⇝ x.
28 ∀R.∀ml:mlattice R.∀xn:sequence ml.increasing ? xn →
29 ∀x,y:ml.supremum ?? xn x → supremum ?? xn y → δ x y ≈ 0.
30 intros (R ml xn Hxn x y Sx Sy);
31 elim (Sx Hxn) (_ Hx); elim (Sy Hxn) (_ Hy);
32 apply (tends_uniq ?? xn ?? Hx Hy);
35 definition shift : ∀R.∀ml:mlattice R.∀xn:sequence ml.nat → sequence ml ≝
36 λR.λml:mlattice R.λxn:sequence ml.λm:nat.λn.xn (n+m).
39 λR.λml:mlattice R.λxn:sequence ml.λk:nat.
40 let rec ank_aux (i : nat) ≝
42 [ O ⇒ (shift ?? xn k) O
43 | S n1 ⇒ (shift ?? xn k) (S n1) ∧ ank_aux n1]
46 notation < "'a'\sup k" non associative with precedence 50 for
49 interpretation "ank" 'ank x k =
50 (cic:/matita/infsup/ank.con _ _ x k).
52 notation < "'a'(k \atop n)" non associative with precedence 50 for
55 interpretation "ank2" 'ank2 x k n =
56 (cic:/matita/infsup/ank.con _ _ x k n).
59 λR.λml:mlattice R.λxn:sequence ml.λk:nat.
60 let rec bnk_aux (i : nat) ≝
62 [ O ⇒ (shift ?? xn k) O
63 | S n1 ⇒ (shift ?? xn k) (S n1) ∨ bnk_aux n1]
67 ∀R.∀ml:mlattice R.∀xn:sequence ml.∀k.decreasing ? (ank ?? xn k).
68 intros (R ml xn k); unfold; intro n; simplify; apply lem;
73 ∀R.∀ml:mlattice R.∀xn:sequence ml.∀k,n:nat.
74 ((ank ?? xn k) (S n)) ≈ (xn k ∧ ank ?? xn (S k) n).
75 intros (R ml xn k n); elim n; simplify; [apply meet_comm]
76 simplify in H; apply (Eq≈ ? (feq_ml ???? (H))); clear H;
77 apply (Eq≈ ? (meet_assoc ????));
78 apply (Eq≈ ?? (eq_sym ??? (meet_assoc ????)));
79 apply feq_mr; rewrite > sym_plus in ⊢ (? ? ? (? ? ? (? (? %))));
80 simplify; rewrite > sym_plus in ⊢ (? ? ? (? ? ? (? (? %))));
86 ∀R.∀ml:mlattice R.∀xn:sequence ml.
87 ∀alpha:sequence ml. (∀k.strong_inf ml (ank ?? xn k) (alpha k)) →
89 intros (R ml xn alpha H); unfold strong_inf in H; unfold lower_bound in H; unfold;
91 letin H2 ≝ (λk.ankS ?? xn k n); clearbody H2;
92 cut (∀k.((xn k) ∧ (ank ?? xn (S k) n)) ≤ (ank ?? xn (S k) n)) as H3; [2:intro k; apply lem;]
93 cut (∀k.(ank ?? xn k (S n)) ≤ (ank ?? xn (S k) n)) as H4; [2:
94 intro k; apply (le_transitive ml ???? (H3 ?));
97 elim (H (S n)) (H4 H5); intro H6; elim (H5 ? H6) (m Hm);
104 lapply (H n) as H1; clear H; elim H1 (LB H); clear H1;
105 lapply (LB (S n)) as H1; clear LB;
106 lapply (ankS ?? xn n n) as H2;
108 lapply (Le≪ (xn n∧ank R ml xn (S n) n) H2);
110 cases H (LB H1); clear H;