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 ≝