definition seg_u ≝
λO:half_ordered_set.λs:segment O.λP: O → CProp.
- wloss O ? (λl,u.P u) (seg_l_ ? s) (seg_u_ ? s).
+ wloss O ? (λl,u.P l) (seg_u_ ? s) (seg_l_ ? s).
definition seg_l ≝
λO:half_ordered_set.λs:segment O.λP: O → CProp.
- wloss O ? (λl,u.P u) (seg_u_ ? s) (seg_l_ ? s).
+ wloss O ? (λl,u.P l) (seg_l_ ? s) (seg_u_ ? s).
interpretation "uppper" 'upp s P = (seg_u (os_l _) s P).
interpretation "lower" 'low s P = (seg_l (os_l _) s P).
definition in_segment ≝
λO:half_ordered_set.λs:segment O.λx:O.
- wloss O ? (λp1,p2.p1 ∧ p2) (seg_u ? s (λu.u ≤≤ x)) (seg_l ? s (λl.x ≤≤ l)).
+ wloss O ? (λp1,p2.p1 ∧ p2) (seg_l ? s (λl.l ≤≤ x)) (seg_u ? s (λu.x ≤≤ u)).
notation "‡O" non associative with precedence 90 for @{'segment $O}.
interpretation "Ordered set sergment" 'segment x = (segment x).
interpretation "segment_preserves_supremum" 'segment_preserves_supremum = (h_segment_preserves_supremum (os_l _)).
interpretation "segment_preserves_infimum" 'segment_preserves_infimum = (h_segment_preserves_supremum (os_r _)).
-(* TEST, ma quanto godo! *)
-lemma segment_preserves_infimum2:
+(*
+test segment_preserves_infimum2:
∀O:ordered_set.∀s:‡O.∀a:sequence {[s]}.∀x:{[s]}.
⌊n,\fst (a n)⌋ is_decreasing ∧
(\fst x) is_infimum ⌊n,\fst (a n)⌋ → a ↓ x.
intros; apply (segment_preserves_infimum s a x H);
qed.
*)
-
+
(* Definition 2.10 *)
+
alias symbol "pi2" = "pair pi2".
alias symbol "pi1" = "pair pi1".
+(*
definition square_segment ≝
- λO:ordered_set.λa,b:O.λx: O squareO.
- And4 (\fst x ≤ b) (a ≤ \fst x) (\snd x ≤ b) (a ≤ \snd x).
-
+ λO:half_ordered_set.λs:segment O.λx: square_half_ordered_set O.
+ in_segment ? s (\fst x) ∧ in_segment ? s (\snd x).
+*)
definition convex ≝
- λO:ordered_set.λU:O squareO → Prop.
- ∀p.U p → \fst p ≤ \snd p → ∀y.
- square_segment O (\fst p) (\snd p) y → U y.
+ λO:half_ordered_set.λU:square_half_ordered_set O → Prop.
+ ∀s.U s → le O (\fst s) (\snd s) →
+ ∀y.
+ le O (\fst y) (\snd s) →
+ le O (\fst s) (\fst y) →
+ le O (\snd y) (\snd s) →
+ le O (\fst y) (\snd y) →
+ U y.
(* Definition 2.11 *)
definition upper_located ≝
lemma h_uparrow_upperlocated:
∀C:half_ordered_set.∀a:sequence C.∀u:C.uparrow ? a u → upper_located ? a.
intros (C a u H); cases H (H2 H3); clear H; intros 3 (x y Hxy);
-cases H3 (H4 H5); clear H3; cases (hos_cotransitive ??? u Hxy) (W W);
-[2: cases (H5 ? W) (w Hw); left; exists [apply w] assumption;
+cases H3 (H4 H5); clear H3; cases (hos_cotransitive C y x u Hxy) (W W);
+[2: cases (H5 x W) (w Hw); left; exists [apply w] assumption;
|1: right; exists [apply u]; split; [apply W|apply H4]]
qed.