alias symbol "nleq" = "Ordered set excess".
alias symbol "leq" = "Ordered set less or equal than".
lemma trans_increasing:
+ ∀C:ordered_set.∀a:sequence C.a is_increasing → ∀n,m:nat_ordered_set. n ≤ m → a n ≤ a m.
+intros 5 (C a Hs n m); elim m; [
+ rewrite > (le_n_O_to_eq n (not_lt_to_le O n H));
+ intro X; cases (os_coreflexive ?? X);]
+cases (le_to_or_lt_eq ?? (not_lt_to_le (S n1) n H1)); clear H1;
+[2: rewrite > H2; intro; cases (os_coreflexive ?? H1);
+|1: apply (le_transitive ???? (H ?) (Hs ?));
+ intro; whd in H1; apply (not_le_Sn_n n); apply (transitive_le ??? H2 H1);]
+qed.
+
+lemma trans_increasing_exc:
∀C:ordered_set.∀a:sequence C.a is_increasing → ∀n,m:nat_ordered_set. m ≰ n → a n ≤ a m.
intros 5 (C a Hs n m); elim m; [cases (not_le_Sn_O n H);]
intro; apply H;
∀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] apply (Hm n);
+[1: intro n; simplify; apply trans_increasing_exc; [assumption] apply (Hm n);
|2: intro n; simplify; apply Uu;
|3: intros (y Hy); simplify; cases (Hu ? Hy);
cases (strictly_increasing_reaches C ? Hm w);
exists [apply w1]; cases (os_cotransitive ??? (a (m w1)) H); [2:assumption]
- cases (trans_increasing C ? Ia ?? H1); assumption;]
+ cases (trans_increasing_exc C ? Ia ?? H1); assumption;]
qed.
(* Definition 2.7 *)
interpretation "Ordered set sergment" 'segment a b =
(cic:/matita/dama/supremum/segment.con _ a b).
-notation "x \in [a,b]" non associative with precedence 50
+notation "hvbox(x \in break [a,b])" non associative with precedence 50
for @{'segment2 $a $b $x}.
interpretation "Ordered set sergment in" 'segment2 a b x=
(cic:/matita/dama/supremum/segment.con _ a b x).
definition pi1 : ∀A.∀P.sigma A P → A ≝ λA,P,s.match s with [sig_in x _ ⇒ x].
-notation < "\pi \sub 1 x" non associative with precedence 50 for @{'pi1 $x}.
-notation < "\pi \sub 2 x" non associative with precedence 50 for @{'pi2 $x}.
+notation < "'fst' \nbsp x" non associative with precedence 50 for @{'pi1 $x}.
+notation < "'snd' \nbsp x" non associative with precedence 50 for @{'pi2 $x}.
notation > "'fst' x" non associative with precedence 50 for @{'pi1 $x}.
notation > "'snd' x" non associative with precedence 50 for @{'pi2 $x}.
interpretation "sigma pi1" 'pi1 x =
(cic:/matita/dama/supremum/pi1.con _ _ x).
-
+
interpretation "Type exists" 'exists \eta.x =
(cic:/matita/dama/supremum/sigma.ind#xpointer(1/1) _ x).
|3: intros 3 (x y z); cases x; cases y ; cases z; simplify; apply os_cotransitive]
qed.
-notation < "{\x|\x \in [a,b]}" non associative with precedence 90
+notation "hvbox({[a, break b]})" non associative with precedence 90
for @{'segment_set $a $b}.
interpretation "Ordered set segment" 'segment_set a b =
(cic:/matita/dama/supremum/segment_ordered_set.con _ a b).
(* Lemma 2.9 *)
lemma segment_preserves_supremum:
- ∀O:ordered_set.∀l,u:O.∀a:sequence (segment_ordered_set ? l u).
- ∀x:(segment_ordered_set ? l u).
+ ∀O:ordered_set.∀l,u:O.∀a:sequence {[l,u]}.∀x:{[l,u]}.
(λn.fst (a n)) is_increasing ∧
(fst x) is_supremum (λn.fst (a n)) → a ↑ x.
intros; split; cases H; clear H;
(cic:/matita/dama/supremum/first.con _ _ x).
interpretation "pair pi2" 'pi2 x =
(cic:/matita/dama/supremum/second.con _ _ x).
+
+notation "hvbox(\langle a, break b\rangle)" non associative with precedence 91 for @{ 'pair $a $b}.
+interpretation "pair" 'pair a b =
+ (cic:/matita/dama/supremum/pair.ind#xpointer(1/1/1) _ _ a b).
+
+notation "a \times b" left associative with precedence 60 for @{'prod $a $b}.
+interpretation "prod" 'prod a b =
+ (cic:/matita/dama/supremum/pair.ind#xpointer(1/1) a b).
lemma square_ordered_set: ordered_set → ordered_set.
-intro O; apply (mk_ordered_set (pair O O));
+intro O; apply (mk_ordered_set (O × O));
[1: intros (x y); apply (fst x ≰ fst y ∨ snd x ≰ snd y);
|2: intro x0; cases x0 (x y); clear x0; simplify; intro H;
cases H (X X); apply (os_coreflexive ?? X);
[1: cases (os_cotransitive ??? z1 H1); [left; left|right;left]assumption;
|2: cases (os_cotransitive ??? z2 H1); [left;right|right;right]assumption]]
qed.
+
+notation < "s 2 \atop \nleq" non associative with precedence 90
+ for @{ 'square $s }.
+notation > "s 'square'" non associative with precedence 90
+ for @{ 'square $s }.
+interpretation "ordered set square" 'square s =
+ (cic:/matita/dama/supremum/square_ordered_set.con s).
definition square_segment ≝
λO:ordered_set.λa,b:O.λx:square_ordered_set O.
(cic:/matita/logic/connectives/And.ind#xpointer(1/1) (snd x ≤ b) (a ≤ snd x))).
definition convex ≝
- λO:ordered_set.λU:square_ordered_set O → Prop.
+ λO:ordered_set.λU:O square → Prop.
∀p.U p → fst p ≤ snd p → ∀y. square_segment ? (fst p) (snd p) y → U y.
(* Definition 2.11 *)
definition upper_located ≝
λO:ordered_set.λa:sequence O.∀x,y:O. y ≰ x →
(∃i:nat.a i ≰ x) ∨ (∃b:O.y≰b ∧ ∀i:nat.a i ≤ b).
+
+definition lower_located ≝
+ λO:ordered_set.λa:sequence O.∀x,y:O. x ≰ y →
+ (∃i:nat.x ≰ a i) ∨ (∃b:O.b≰y ∧ ∀i:nat.b ≤ a i).
+
+notation < "s \nbsp 'is_upper_located'" non associative with precedence 50
+ for @{'upper_located $s}.
+notation > "s 'is_upper_located'" non associative with precedence 50
+ for @{'upper_located $s}.
+interpretation "Ordered set upper locatedness" 'upper_located s =
+ (cic:/matita/dama/supremum/upper_located.con _ s).
+
+notation < "s \nbsp 'is_lower_located'" non associative with precedence 50
+ for @{'lower_located $s}.
+notation > "s 'is_lower_located'" non associative with precedence 50
+ for @{'lower_located $s}.
+interpretation "Ordered set lower locatedness" 'lower_located s =
+ (cic:/matita/dama/supremum/lower_located.con _ s).
(* Lemma 2.12 *)
-lemma uparrow_located:
- ∀C:ordered_set.∀a:sequence C.∀u:C.a ↑ u → upper_located ? a.
+lemma uparrow_upperlocated:
+ ∀C:ordered_set.∀a:sequence C.∀u:C.a ↑ u → a is_upper_located.
intros (C a u H); cases H (H2 H3); clear H; intros 3 (x y Hxy);
cases H3 (H4 H5); clear H3; cases (os_cotransitive ??? u Hxy) (W W);
[2: cases (H5 ? W) (w Hw); left; exists [apply w] assumption;
|1: right; exists [apply u]; split; [apply W|apply H4]]
qed.
+lemma downarrow_lowerlocated:
+ ∀C:ordered_set.∀a:sequence C.∀u:C.a ↓ u → a is_lower_located.
+intros (C a u H); cases H (H2 H3); clear H; intros 3 (x y Hxy);
+cases H3 (H4 H5); clear H3; cases (os_cotransitive ??? u Hxy) (W W);
+[1: cases (H5 ? W) (w Hw); left; exists [apply w] assumption;
+|2: right; exists [apply u]; split; [apply W|apply H4]]
+qed.
\ No newline at end of file
projects / helm.git / blobdiff