lemma le_le_eq: ∀E:ordered_set.∀a,b:E. a ≤ b → b ≤ a → a ≈ b.
intros (E x y L1 L2); intro H; cases H; [apply L1|apply L2] assumption;
qed.
+
+definition lt ≝ λE:ordered_set.λa,b:E. a ≤ b ∧ a # b.
+
+interpretation "ordered sets less than" 'lt a b =
+ (cic:/matita/dama/bishop_set/lt.con _ a b).
+
+lemma lt_coreflexive: ∀E.coreflexive ? (lt E).
+intros 2 (E x); intro H; cases H (_ ABS);
+apply (bs_coreflexive ? x ABS);
+qed.
+
+lemma lt_transitive: ∀E.transitive ? (lt E).
+intros (E); unfold; intros (x y z H1 H2); cases H1 (Lxy Axy); cases H2 (Lyz Ayz);
+split; [apply (le_transitive ???? Lxy Lyz)] clear H1 H2;
+cases Axy (H1 H1); cases Ayz (H2 H2); [1:cases (Lxy H1)|3:cases (Lyz H2)]clear Axy Ayz;
+[1: cases (os_cotransitive ??? y H1) (X X); [cases (Lxy X)|cases (os_coreflexive ?? X)]
+|2: cases (os_cotransitive ??? x H2) (X X); [right;assumption|cases (Lxy X)]]
+qed.
+
+theorem lt_to_excess: ∀E:ordered_set.∀a,b:E. (a < b) → (b ≰ a).
+intros (E a b Lab); cases Lab (LEab Aab); cases Aab (H H);[cases (LEab H)]
+assumption;
+qed.
(* Definition 2.4 *)
definition upper_bound ≝ λO:ordered_set.λa:sequence O.λu:O.∀n:nat.a n ≤ u.
-definition strong_sup ≝
+definition supremum ≝
λO:ordered_set.λs:sequence O.λx.upper_bound ? s x ∧ (∀y:O.x ≰ y → ∃n.s n ≰ y).
definition increasing ≝ λO:ordered_set.λa:sequence O.∀n:nat.a n ≤ a (S n).
for @{'upper_bound $s $x}.
notation < "s \nbsp 'is_increasing'" non associative with precedence 50
for @{'increasing $s}.
-notation < "x \nbsp 'is_strong_sup' \nbsp s" non associative with precedence 50
- for @{'strong_sup $s $x}.
+notation < "x \nbsp 'is_supremum' \nbsp s" non associative with precedence 50
+ for @{'supremum $s $x}.
notation > "x 'is_upper_bound' s" non associative with precedence 50
for @{'upper_bound $s $x}.
notation > "s 'is_increasing'" non associative with precedence 50
for @{'increasing $s}.
-notation > "x 'is_strong_sup' s" non associative with precedence 50
- for @{'strong_sup $s $x}.
+notation > "x 'is_supremum' s" non associative with precedence 50
+ for @{'supremum $s $x}.
interpretation "Ordered set upper bound" 'upper_bound s x =
(cic:/matita/dama/supremum/upper_bound.con _ s x).
interpretation "Ordered set increasing" 'increasing s =
(cic:/matita/dama/supremum/increasing.con _ s).
-interpretation "Ordered set strong sup" 'strong_sup s x =
- (cic:/matita/dama/supremum/strong_sup.con _ s x).
+interpretation "Ordered set strong sup" 'supremum s x =
+ (cic:/matita/dama/supremum/supremum.con _ s x).
-include "bishop_set.ma".
+include "nat/compare.ma".
+include "nat/plus.ma".
+include "bishop_set.ma".
lemma uniq_supremum:
∀O:ordered_set.∀s:sequence O.∀t1,t2:O.
- t1 is_strong_sup s → t2 is_strong_sup s → t1 ≈ t2.
+ t1 is_supremum s → t2 is_supremum s → t1 ≈ t2.
intros (O s t1 t2 Ht1 Ht2); cases Ht1 (U1 H1); cases Ht2 (U2 H2);
apply le_le_eq; intro X;
[1: cases (H1 ? X); apply (U2 w); assumption
|2: cases (H2 ? X); apply (U1 w); assumption]
qed.
+(* Fact 2.5 *)
+lemma supremum_is_upper_bound:
+ ∀C:ordered_set.∀a:sequence C.∀u:C.
+ u is_supremum a → ∀v.v is_upper_bound a → u ≤ v.
+intros 7 (C s u Hu v Hv H); cases Hu (_ H1); clear Hu;
+cases (H1 ? H) (w Hw); apply Hv; assumption;
+qed.
+
+(* Lemma 2.6 *)
+definition strictly_increasing ≝ λC:ordered_set.λa:sequence C.∀n:nat.a (S n) ≰ a n.
+
+definition nat_excess : nat → nat → CProp ≝ λn,m. leb (m+S O) n = true.
+
+axiom nat_excess_cotransitive: cotransitive ? nat_excess.
+(*intros 3 (x y z); elim x 0; elim y 0; elim z 0;
+ [1: intros; left; assumption
+ |2,5,6,7: intros; first [right; constructor 1|left; constructor 1]
+ |3: intros (n H abs); simplify in abs; destruct abs;
+ |4: intros (n H m W abs); simplify in abs; destruct abs;
+ |8: clear x y z; intros (x H1 y H2 z H3 H4);
+*)
+
+lemma nat_ordered_set : ordered_set.
+apply (mk_ordered_set ? nat_excess);
+[1: intro x; elim x (w H); simplify; intro X; [destruct X] apply H; assumption;
+|2: apply nat_excess_cotransitive]
+qed.
-
+notation < "s \nbsp 'is_strictly_increasing'" non associative with precedence 50
+ for @{'strictly_increasing $s}.
+notation > "s 'is_strictly_increasing'" non associative with precedence 50
+ for @{'strictly_increasing $s}.
+interpretation "Ordered set increasing" 'strictly_increasing s =
+ (cic:/matita/dama/supremum/strictly_increasing.con _ s).
+
+notation "a \uparrow u" non associative with precedence 50 for @{'sup_inc $a $u}.
+interpretation "Ordered set supremum of increasing" 'sup_inc s u =
+ (cic:/matita/dama/cprop_connectives/And.ind#xpointer(1/1)
+ (cic:/matita/dama/supremum/increasing.con _ s)
+ (cic:/matita/dama/supremum/supremum.con _ s u)).
+
+lemma trans_increasing:
+ ∀C:ordered_set.∀s:sequence C.s is_increasing → ∀n,m. m ≰ n → s n ≤ s m.
+intros 5 (C s Hs n m); elim m; [1: cases (?:False); autobatch]
+cases (le_to_or_lt_eq ?? H1);
+ [2: destruct H2; apply Hs;
+ |1: apply (le_transitive ???? (H (lt_S_S_to_lt ?? H2))); apply Hs;]
+qed.
+
+lemma selection:
+ ∀C:ordered_set.∀m:sequence nat_ordered_set.m is_strictly_increasing →
+ ∀a:sequence C.∀u.a ↑ u → (λx.a (m x)) ↑ u.
+intros (C m Hm a u Ha); cases Ha (Ia Su); cases Su (Uu Hu); repeat split;
+[1: intro n; simplify; apply trans_increasing; [assumption]
+ lapply (Hm n) as W; unfold nat_ordered_set in W; simplify in W;
+ cases W;
+|2: intro n;
+|3:
+
\ No newline at end of file
projects / helm.git / commitdiff