helm/software/matita/contribs/dama/dama/supremum.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 include "ordered_set.ma".
  17
  18 (* Definition 2.4 *)
  19 definition upper_bound ≝ λO:ordered_set.λa:sequence O.λu:O.∀n:nat.a n ≤ u.
  20
  21 definition strong_sup ≝
  22   λO:ordered_set.λs:sequence O.λx.upper_bound ? s x ∧ (∀y:O.x ≰ y → ∃n.s n ≰ y).
  23
  24 definition increasing ≝ λO:ordered_set.λa:sequence O.∀n:nat.a n ≤ a (S n).
  25
  26 notation < "x \nbsp 'is_upper_bound' \nbsp s" non associative with precedence 50
  27   for @{'upper_bound $s $x}.
  28 notation < "s \nbsp 'is_increasing'"          non associative with precedence 50
  29   for @{'increasing $s}.
  30 notation < "x \nbsp 'is_strong_sup' \nbsp s"  non associative with precedence 50
  31   for @{'strong_sup $s $x}.
  32
  33 notation > "x 'is_upper_bound' s" non associative with precedence 50
  34   for @{'upper_bound $s $x}.
  35 notation > "s 'is_increasing'"    non associative with precedence 50
  36   for @{'increasing $s}.
  37 notation > "x 'is_strong_sup' s"  non associative with precedence 50
  38   for @{'strong_sup $s $x}.
  39
  40 interpretation "Ordered set upper bound" 'upper_bound s x =
  41   (cic:/matita/dama/supremum/upper_bound.con _ s x).
  42 interpretation "Ordered set increasing"  'increasing s    =
  43   (cic:/matita/dama/supremum/increasing.con _ s).
  44 interpretation "Ordered set strong sup"  'strong_sup s x  =
  45   (cic:/matita/dama/supremum/strong_sup.con _ s x).
  46
  47 include "bishop_set.ma".
  48
  49 lemma uniq_supremum:
  50   ∀O:ordered_set.∀s:sequence O.∀t1,t2:O.
  51     t1 is_upper_bound s → t2 is_upper_bound s → t1 ≈ t2.
  52 intros (O s t1 t2 Ht1 Ht2); apply le_le_eq; cases Ht1; cases Ht2;
  53