X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fmatita%2Fdama%2Finfsup.ma;h=cc3292fd0b5178775d5199ba3bc5d850570a6e38;hb=8da8820a77f2104dd1bf17c01fa77f75ee31c8fb;hp=60c4d2f81a5c62ef45a40b4ad8e824113114ceea;hpb=9483f7e6c85ec11f88bdb219b2cebad2039b1a74;p=helm.git

diff --git a/helm/software/matita/dama/infsup.ma b/helm/software/matita/dama/infsup.ma
index 60c4d2f81..cc3292fd0 100644
--- a/helm/software/matita/dama/infsup.ma
+++ b/helm/software/matita/dama/infsup.ma
@@ -16,34 +16,38 @@ include "sequence.ma".
 
 definition upper_bound ≝ λO:excess.λa:sequence O.λu:O.∀n:nat.a n ≤ u.
 
+definition weak_sup ≝
+  λO:excess.λs:sequence O.λx.
+    upper_bound ? s x ∧ (∀y:O.upper_bound ? s y → x ≤ y).
+
 definition strong_sup ≝
   λO:excess.λs:sequence O.λx.upper_bound ? s x ∧ (∀y:O.x ≰ y → ∃n.s n ≰ y).
 
 definition increasing ≝ λO:excess.λa:sequence O.∀n:nat.a n ≤ a (S n).
 
-notation < "x \nbsp 'is_upper_bound' \nbsp s" non associative with precedence 50 for @{'upper_bound $s $x}.
-notation < "x \nbsp 'is_lower_bound' \nbsp s" non associative with precedence 50 for @{'lower_bound $s $x}.
-notation < "s \nbsp 'is_increasing'"          non associative with precedence 50 for @{'increasing $s}.
-notation < "s \nbsp 'is_decreasing'"          non associative with precedence 50 for @{'decreasing $s}.
-notation < "x \nbsp 'is_strong_sup' \nbsp s"  non associative with precedence 50 for @{'strong_sup $s $x}.
-notation < "x \nbsp 'is_strong_inf' \nbsp s"  non associative with precedence 50 for @{'strong_inf $s $x}.
-
-notation > "x 'is_upper_bound' s" non associative with precedence 50 for @{'upper_bound $s $x}.
-notation > "x 'is_lower_bound' s" non associative with precedence 50 for @{'lower_bound $s $x}.
-notation > "s 'is_increasing'"    non associative with precedence 50 for @{'increasing $s}.
-notation > "s 'is_decreasing'"    non associative with precedence 50 for @{'decreasing $s}.
-notation > "x 'is_strong_sup' s"  non associative with precedence 50 for @{'strong_sup $s $x}.
-notation > "x 'is_strong_inf' s"  non associative with precedence 50 for @{'strong_inf $s $x}.
-
-interpretation "Excess upper bound" 'upper_bound s x = (cic:/matita/infsup/upper_bound.con _ s x).
-interpretation "Excess lower bound" 'lower_bound s x = (cic:/matita/infsup/upper_bound.con (cic:/matita/excess/dual_exc.con _) s x).
-interpretation "Excess increasing"  'increasing s    = (cic:/matita/infsup/increasing.con _ s).
-interpretation "Excess decreasing"  'decreasing s    = (cic:/matita/infsup/increasing.con (cic:/matita/excess/dual_exc.con _) s).
-interpretation "Excess strong sup"  'strong_sup s x  = (cic:/matita/infsup/strong_sup.con _ s x).
-interpretation "Excess strong inf"  'strong_inf s x  = (cic:/matita/infsup/strong_sup.con (cic:/matita/excess/dual_exc.con _) s x).
-
-definition seq_dual_exc_hint: ∀E.sequence E → sequence (dual_exc E) ≝ λE.λx:sequence E.x.
-definition seq_dual_exc_hint1: ∀E.sequence (dual_exc E) → sequence E ≝ λE.λx:sequence (dual_exc E).x.
-
-coercion cic:/matita/infsup/seq_dual_exc_hint.con nocomposites.
-coercion cic:/matita/infsup/seq_dual_exc_hint1.con nocomposites.
+notation < "x \nbsp 'is_upper_bound' \nbsp s" non associative with precedence 50 for @{'upper_bound $_ $s $x}.
+notation < "x \nbsp 'is_lower_bound' \nbsp s" non associative with precedence 50 for @{'lower_bound $_ $s $x}.
+notation < "s \nbsp 'is_increasing'"          non associative with precedence 50 for @{'increasing $_ $s}.
+notation < "s \nbsp 'is_decreasing'"          non associative with precedence 50 for @{'decreasing $_ $s}.
+notation < "x \nbsp 'is_strong_sup' \nbsp s"  non associative with precedence 50 for @{'strong_sup $_ $s $x}.
+notation < "x \nbsp 'is_strong_inf' \nbsp s"  non associative with precedence 50 for @{'strong_inf $_ $s $x}.
+
+notation > "x 'is_upper_bound' s 'in' e" non associative with precedence 50 for @{'upper_bound $e $s $x}.
+notation > "x 'is_lower_bound' s 'in' e" non associative with precedence 50 for @{'lower_bound $e $s $x}.
+notation > "s 'is_increasing' 'in' e"    non associative with precedence 50 for @{'increasing $e $s}.
+notation > "s 'is_decreasing' 'in' e"    non associative with precedence 50 for @{'decreasing $e $s}.
+notation > "x 'is_strong_sup' s 'in' e"  non associative with precedence 50 for @{'strong_sup $e $s $x}.
+notation > "x 'is_strong_inf' s 'in' e"  non associative with precedence 50 for @{'strong_inf $e $s $x}.
+
+interpretation "Excess upper bound" 'upper_bound e s x = (cic:/matita/infsup/upper_bound.con e s x).
+interpretation "Excess lower bound" 'lower_bound e s x = (cic:/matita/infsup/upper_bound.con (cic:/matita/excess/dual_exc.con e) s x).
+interpretation "Excess increasing"  'increasing e s    = (cic:/matita/infsup/increasing.con e s).
+interpretation "Excess decreasing"  'decreasing e s    = (cic:/matita/infsup/increasing.con (cic:/matita/excess/dual_exc.con e) s).
+interpretation "Excess strong sup"  'strong_sup e s x  = (cic:/matita/infsup/strong_sup.con e s x).
+interpretation "Excess strong inf"  'strong_inf e s x  = (cic:/matita/infsup/strong_sup.con (cic:/matita/excess/dual_exc.con e) s x).
+
+lemma strong_sup_is_weak: 
+  ∀O:excess.∀s:sequence O.∀x:O.strong_sup ? s x → weak_sup ? s x.
+intros (O s x Ssup); elim Ssup (Ubx M); clear Ssup; split; [assumption]
+intros 3 (y Uby E); cases (M ? E) (n En); unfold in Uby; cases (Uby ? En);
+qed.