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 ⊢ (? ? ? (? ? ? (? (? %))));
85 ∀R.∀ml:mlattice R.∀xn:sequence ml.∀k,n.
86 (ank ?? xn k (S n)) ≤ (ank ?? xn (S k) n).
88 apply (Le≪ (xn k ∧ ank ?? xn (S k) n) (ankS ?????)); apply lem;
93 ∀R.∀ml:mlattice R.∀xn:sequence ml.
94 ∀alpha:sequence ml. (∀k.strong_inf ml (ank ?? xn k) (alpha k)) →
96 intros (R ml xn alpha H); unfold strong_inf in H; unfold lower_bound in H; unfold;
99 elim (H (S r)) (H1sr H2sr); clear H H2r H1sr;
100 intro e; cases (H2sr ? e) (w Hw); clear e H2sr;
101 lapply (H1r (S w)) as Hsw; clear H1r;
102 lapply (le_transitive ???? Hsw (le_asnk_ansk ?????)) as H;