helm/software/matita/dama/limit.ma

   1 (**************************************************************************)
   2 (*       ___                                                              *)
   3 (*      ||M||                                                             *)
   4 (*      ||A||       A project by Andrea Asperti                           *)
   5 (*      ||T||                                                             *)
   6 (*      ||I||       Developers:                                           *)
   7 (*      ||T||         The HELM team.                                      *)
   8 (*      ||A||         http://helm.cs.unibo.it                             *)
   9 (*      \   /                                                             *)
  10 (*       \ /        This file is distributed under the terms of the       *)
  11 (*        v         GNU General Public License Version 2                  *)
  12 (*                                                                        *)
  13 (**************************************************************************)
  14
  15 include "infsup.ma".
  16
  17 (* 3.28 *)
  18 definition limsup ≝
  19   λE:excess.λxn:sequence E.λx:E.∃alpha:sequence E.
  20     (∀k.(alpha k) is_strong_sup xn) ∧ x is_strong_inf alpha.
  21
  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}.
  26
  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).
  29
  30 (* 3.29 *)
  31 definition lim ≝ λE:excess.λxn:sequence E.λx:E. x is_limsup xn ∧ x is_liminf xn.
  32
  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).
  36
  37 lemma sup_decreasing:
  38   ∀E:excess.∀xn:sequence E.
  39    ∀alpha:sequence E. (∀k.(alpha k) is_strong_sup xn) →
  40      alpha is_decreasing.
  41 intros (E xn alpha H); unfold strong_sup in H; unfold upper_bound in H; unfold;
  42 intro r;
  43 elim (H r) (H1r H2r);
  44 elim (H (S r)) (H1sr H2sr); clear H H2r H1sr;
  45 intro e; cases (H2sr (alpha r) e) (w Hw); clear e H2sr;
  46 cases (H1r w Hw);
  47 qed.
  48
  49 include "tend.ma".
  50
  51 (* 3.30 *)
  52 lemma lim_tends:
  53   ∀R.∀ml:mlattice R.∀xn:sequence ml.∀x:ml.
  54     x is_lim xn → xn ⇝ x.
  55 intros (R ml xn x Hl); unfold lim in Hl; unfold limsup in Hl;
  56