helm/software/matita/dama/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 strong_sup ≝
  20   λO:excess.λs:sequence O.λx.upper_bound ? s x ∧ (∀y:O.x ≰ y → ∃n.s n ≰ y).
  21
  22 definition increasing ≝ λO:excess.λa:sequence O.∀n:nat.a n ≤ a (S n).
  23
  24 notation < "x \nbsp 'is_upper_bound' \nbsp s" non associative with precedence 50 for @{'upper_bound $s $x}.
  25 notation < "x \nbsp 'is_lower_bound' \nbsp s" non associative with precedence 50 for @{'lower_bound $s $x}.
  26 notation < "s \nbsp 'is_increasing'"          non associative with precedence 50 for @{'increasing $s}.
  27 notation < "s \nbsp 'is_decreasing'"          non associative with precedence 50 for @{'decreasing $s}.
  28 notation < "x \nbsp 'is_strong_sup' \nbsp s"  non associative with precedence 50 for @{'strong_sup $s $x}.
  29 notation < "x \nbsp 'is_strong_inf' \nbsp s"  non associative with precedence 50 for @{'strong_inf $s $x}.
  30
  31 notation > "x 'is_upper_bound' s" non associative with precedence 50 for @{'upper_bound $s $x}.
  32 notation > "x 'is_lower_bound' s" non associative with precedence 50 for @{'lower_bound $s $x}.
  33 notation > "s 'is_increasing'"    non associative with precedence 50 for @{'increasing $s}.
  34 notation > "s 'is_decreasing'"    non associative with precedence 50 for @{'decreasing $s}.
  35 notation > "x 'is_strong_sup' s"  non associative with precedence 50 for @{'strong_sup $s $x}.
  36 notation > "x 'is_strong_inf' s"  non associative with precedence 50 for @{'strong_inf $s $x}.
  37
  38 interpretation "Excess upper bound" 'upper_bound s x = (cic:/matita/infsup/upper_bound.con _ s x).
  39 interpretation "Excess lower bound" 'lower_bound s x = (cic:/matita/infsup/upper_bound.con (cic:/matita/excess/dual_exc.con _) s x).
  40 interpretation "Excess increasing"  'increasing s    = (cic:/matita/infsup/increasing.con _ s).
  41 interpretation "Excess decreasing"  'decreasing s    = (cic:/matita/infsup/increasing.con (cic:/matita/excess/dual_exc.con _) s).
  42 interpretation "Excess strong sup"  'strong_sup s x  = (cic:/matita/infsup/strong_sup.con _ s x).
  43 interpretation "Excess strong inf"  'strong_inf s x  = (cic:/matita/infsup/strong_sup.con (cic:/matita/excess/dual_exc.con _) s x).
  44
  45 definition seq_dual_exc_hint: ∀E.sequence E → sequence (dual_exc E) ≝ λE.λx:sequence E.x.
  46 definition seq_dual_exc_hint1: ∀E.sequence (dual_exc E) → sequence E ≝ λE.λx:sequence (dual_exc E).x.
  47
  48 coercion cic:/matita/infsup/seq_dual_exc_hint.con nocomposites.
  49 coercion cic:/matita/infsup/seq_dual_exc_hint1.con nocomposites.