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 (**************************************************************************)
19 λE:excess.λxn:sequence E.λx:E.∃alpha:sequence E.
20 (∀k.(alpha k) is_strong_sup xn) ∧ x is_strong_inf alpha.
22 notation < "x \nbsp 'is_limsup' \nbsp s" non associative with precedence 50 for @{'limsup $s $x}.
23 notation < "x \nbsp 'is_liminf' \nbsp s" non associative with precedence 50 for @{'liminf $s $x}.
24 notation > "x 'is_limsup' s" non associative with precedence 50 for @{'limsup $s $x}.
25 notation > "x 'is_liminf' s" non associative with precedence 50 for @{'liminf $s $x}.
27 interpretation "Excess limsup" 'limsup s x = (cic:/matita/limit/limsup.con _ s x).
28 interpretation "Excess liminf" 'liminf s x = (cic:/matita/limit/limsup.con (cic:/matita/excess/dual_exc.con _) s x).
31 definition lim ≝ λE:excess.λxn:sequence E.λx:E. x is_limsup xn ∧ x is_liminf xn.
33 notation < "x \nbsp 'is_lim' \nbsp s" non associative with precedence 50 for @{'lim $s $x}.
34 notation > "x 'is_lim' s" non associative with precedence 50 for @{'lim $s $x}.
35 interpretation "Excess lim" 'lim s x = (cic:/matita/limit/lim.con _ s x).
38 ∀E:excess.∀xn:sequence E.
39 ∀alpha:sequence E. (∀k.(alpha k) is_strong_sup xn) →
41 intros (E xn alpha H); unfold strong_sup in H; unfold upper_bound in H; unfold;
44 elim (H (S r)) (H1sr H2sr); clear H H2r H1sr;
45 intro e; cases (H2sr (alpha r) e) (w Hw); clear e H2sr;
53 ∀R.∀ml:mlattice R.∀xn:sequence ml.∀x:ml.
55 intros (R ml xn x Hl); unfold lim in Hl; unfold limsup in Hl;