(* Definition 2.7 *)
definition order_converge ≝
λO:ordered_set.λa:sequence O.λx:O.
- ExT23 (sequence O) (λl.l ↑ x) (λu.u ↓ x)
- (λl,u.∀i:nat. (l i) is_infimum ⌊w,a (w+i)⌋ ∧
+ exT23 (sequence O) (λl.l ↑ x) (λu.u ↓ x)
+ (λl,u:sequence O.∀i:nat. (l i) is_infimum ⌊w,a (w+i)⌋ ∧
(u i) is_supremum ⌊w,a (w+i)⌋).
-notation < "a \nbsp (\circ \atop (\horbar\triangleright)) \nbsp x" non associative with precedence 45
+notation < "a \nbsp (\cir \atop (\horbar\triangleright)) \nbsp x" non associative with precedence 45
for @{'order_converge $a $x}.
notation > "a 'order_converges' x" non associative with precedence 45
for @{'order_converge $a $x}.
lemma segment_ordered_set:
∀O:ordered_set.∀u,v:O.ordered_set.
intros (O u v); apply (mk_ordered_set (∃x.x ∈ [u,v]));
-[1: intros (x y); apply (fst x ≰ fst y);
+[1: intros (x y); apply (\fst x ≰ \fst y);
|2: intro x; cases x; simplify; apply os_coreflexive;
|3: intros 3 (x y z); cases x; cases y ; cases z; simplify; apply os_cotransitive]
qed.
(* Lemma 2.9 *)
lemma segment_preserves_supremum:
∀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.
+ ⌊n,\fst (a n)⌋ is_increasing ∧
+ (\fst x) is_supremum ⌊n,\fst (a n)⌋ → a ↑ x.
intros; split; cases H; clear H;
[1: apply H1;
|2: cases H2; split; clear H2;
[1: apply H;
- |2: clear H; intro y0; apply (H3 (fst y0));]]
+ |2: clear H; intro y0; apply (H3 (\fst y0));]]
qed.
lemma segment_preserves_infimum:
∀O:ordered_set.∀l,u:O.∀a:sequence {[l,u]}.∀x:{[l,u]}.
- ⌊n,fst (a n)⌋ is_decreasing ∧
- (fst x) is_infimum ⌊n,fst (a n)⌋ → a ↓ x.
+ ⌊n,\fst (a n)⌋ is_decreasing ∧
+ (\fst x) is_infimum ⌊n,\fst (a n)⌋ → a ↓ x.
intros; split; cases H; clear H;
[1: apply H1;
|2: cases H2; split; clear H2;
[1: apply H;
- |2: clear H; intro y0; apply (H3 (fst y0));]]
+ |2: clear H; intro y0; apply (H3 (\fst y0));]]
qed.
(* Definition 2.10 *)
alias symbol "pi1" = "pair pi1".
definition square_segment ≝
λO:ordered_set.λa,b:O.λx:O square.
- And4 (fst x ≤ b) (a ≤ fst x) (snd x ≤ b) (a ≤ snd x).
+ And4 (\fst x ≤ b) (a ≤ \fst x) (\snd x ≤ b) (a ≤ \snd x).
definition convex ≝
λO:ordered_set.λU:O square → Prop.
- ∀p.U p → fst p ≤ snd p → ∀y. square_segment ? (fst p) (snd p) y → U y.
+ ∀p.U p → \fst p ≤ \snd p → ∀y. square_segment ? (\fst p) (\snd p) y → U y.
(* Definition 2.11 *)
definition upper_located ≝