(* Definition 2.7 *)
definition order_converge ≝
λO:ordered_set.λa:sequence O.λx:O.
- ExT23 (sequence O) (λl.l ↑ x) (λu.u ↓ x)
+ exT23 (sequence O) (λl.l ↑ x) (λu.u ↓ x)
(λl,u.∀i:nat. (l i) is_infimum ⌊w,a (w+i)⌋ ∧
(u i) is_supremum ⌊w,a (w+i)⌋).
for @{'segment_in $a $b $x}.
interpretation "Ordered set sergment in" 'segment_in a b x= (segment _ a b x).
-(*
-coinductive sigma (A:Type) (P:A→Prop) : Type ≝ sig_in : ∀x.P x → sigma A P.
-
-definition pi1sig : ∀A.∀P.sigma A P → A ≝ λA,P,s.match s with [sig_in x _ ⇒ x].
-
-interpretation "sigma pi1" 'pi1a x = (pi1sig _ _ x).
-
-interpretation "Type exists" 'exists \eta.x = (sigma _ 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]));
qed.
(* Definition 2.10 *)
-coinductive pair (A,B:Type) : Type ≝ prod : ∀a:A.∀b:B.pair A B.
-definition first : ∀A.∀P.pair A P → A ≝ λA,P,s.match s with [prod x _ ⇒ x].
-definition second : ∀A.∀P.pair A P → P ≝ λA,P,s.match s with [prod _ y ⇒ y].
-
-interpretation "pair pi1" 'pi1 = (first _ _).
-interpretation "pair pi2" 'pi2 = (second _ _).
-interpretation "pair pi1" 'pi1a x = (first _ _ x).
-interpretation "pair pi2" 'pi2a x = (second _ _ x).
-interpretation "pair pi1" 'pi1b x y = (first _ _ x y).
-interpretation "pair pi2" 'pi2b x y = (second _ _ x y).
-
-notation "hvbox(\langle a, break b\rangle)" left associative with precedence 70 for @{ 'pair $a $b}.
-interpretation "pair" 'pair a b = (prod _ _ a b).
-interpretation "prod" 'product a b = (pair a b).
-
-lemma square_ordered_set: ordered_set → ordered_set.
-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);
-|3: intros 3 (x0 y0 z0); cases x0 (x1 x2); cases y0 (y1 y2) ; cases z0 (z1 z2);
- clear x0 y0 z0; simplify; intro H; cases H (H1 H1); clear H;
- [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 = (square_ordered_set s).
-
+alias symbol "square" = "ordered set square".
+alias symbol "pi2" = "pair pi2".
+alias symbol "pi1" = "pair pi1".
definition square_segment ≝
- λO:ordered_set.λa,b:O.λx:square_ordered_set O.
+ λO:ordered_set.λa,b:O.λx:O square.
And4 (fst x ≤ b) (a ≤ fst x) (snd x ≤ b) (a ≤ snd x).
definition convex ≝