matita/matita/contribs/dama/dama_duality/infsup.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 "sequence.ma".
  16
  17 definition upper_bound ≝ λO:excess.λa:sequence O.λu:O.∀n:nat.a n ≤ u.
  18
  19 definition weak_sup ≝
  20   λO:excess.λs:sequence O.λx.
  21     upper_bound ? s x ∧ (∀y:O.upper_bound ? s y → x ≤ y).
  22
  23 definition strong_sup ≝
  24   λO:excess.λs:sequence O.λx.upper_bound ? s x ∧ (∀y:O.x ≰ y → ∃n.s n ≰ y).
  25
  26 definition increasing ≝ λO:excess.λa:sequence O.∀n:nat.a n ≤ a (S n).
  27
  28 notation < "x \nbsp 'is_upper_bound' \nbsp s" non associative with precedence 55 for @{'upper_bound $_ $s $x}.
  29 notation < "x \nbsp 'is_lower_bound' \nbsp s" non associative with precedence 55 for @{'lower_bound $_ $s $x}.
  30 notation < "s \nbsp 'is_increasing'"          non associative with precedence 55 for @{'increasing $_ $s}.
  31 notation < "s \nbsp 'is_decreasing'"          non associative with precedence 55 for @{'decreasing $_ $s}.
  32 notation < "x \nbsp 'is_strong_sup' \nbsp s"  non associative with precedence 55 for @{'strong_sup $_ $s $x}.
  33 notation < "x \nbsp 'is_strong_inf' \nbsp s"  non associative with precedence 55 for @{'strong_inf $_ $s $x}.
  34
  35 notation > "x 'is_upper_bound' s 'in' e" non associative with precedence 55 for @{'upper_bound $e $s $x}.
  36 notation > "x 'is_lower_bound' s 'in' e" non associative with precedence 55 for @{'lower_bound $e $s $x}.
  37 notation > "s 'is_increasing' 'in' e"    non associative with precedence 55 for @{'increasing $e $s}.
  38 notation > "s 'is_decreasing' 'in' e"    non associative with precedence 55 for @{'decreasing $e $s}.
  39 notation > "x 'is_strong_sup' s 'in' e"  non associative with precedence 55 for @{'strong_sup $e $s $x}.
  40 notation > "x 'is_strong_inf' s 'in' e"  non associative with precedence 55 for @{'strong_inf $e $s $x}.
  41
  42 interpretation "Excess upper bound" 'upper_bound e s x = (upper_bound e s x).
  43 interpretation "Excess lower bound" 'lower_bound e s x = (upper_bound (dual_exc e) s x).
  44 interpretation "Excess increasing"  'increasing e s    = (increasing e s).
  45 interpretation "Excess decreasing"  'decreasing e s    = (increasing (dual_exc e) s).
  46 interpretation "Excess strong sup"  'strong_sup e s x  = (strong_sup e s x).
  47 interpretation "Excess strong inf"  'strong_inf e s x  = (strong_sup (dual_exc e) s x).
  48
  49 lemma strong_sup_is_weak:
  50   ∀O:excess.∀s:sequence O.∀x:O.strong_sup ? s x → weak_sup ? s x.
  51 intros (O s x Ssup); elim Ssup (Ubx M); clear Ssup; split; [assumption]
  52 intros 3 (y Uby E); cases (M ? E) (n En); unfold in Uby; cases (Uby ? En);
  53 qed.