seg_u_ : O
}.
-notation > "𝕦_term 90 s p" non associative with precedence 45 for @{'upp $s $p}.
-notation "𝕦 \sub term 90 s p" non associative with precedence 45 for @{'upp $s $p}.
-notation > "𝕝_term 90 s p" non associative with precedence 45 for @{'low $s $p}.
-notation "𝕝 \sub term 90 s p" non associative with precedence 45 for @{'low $s $p}.
+notation > "𝕦_term 90 s" non associative with precedence 90 for @{'upp $s}.
+notation "𝕦 \sub term 90 s" non associative with precedence 90 for @{'upp $s}.
+notation > "𝕝_term 90 s" non associative with precedence 90 for @{'low $s}.
+notation "𝕝 \sub term 90 s" non associative with precedence 90 for @{'low $s}.
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).
+ λO:half_ordered_set.λs:segment O.
+ wloss O ?? (λl,u.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).
+ λO:half_ordered_set.λs:segment O.
+ wloss O ?? (λl,u.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).
-interpretation "uppper dual" 'upp s P = (seg_l (os_r _) s P).
-interpretation "lower dual" 'low s P = (seg_u (os_r _) s P).
+interpretation "uppper" 'upp s = (seg_u (os_l _) s).
+interpretation "lower" 'low s = (seg_l (os_l _) s).
+interpretation "uppper dual" 'upp s = (seg_l (os_r _) s).
+interpretation "lower dual" 'low s = (seg_u (os_r _) s).
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 ≤≤ x) (x ≤≤ seg_u ? s).
notation "‡O" non associative with precedence 90 for @{'segment $O}.
interpretation "Ordered set sergment" 'segment x = (segment x).
λO:half_ordered_set.λs:‡O.
λx,y:segment_ordered_set_carr O s.hos_excess_ O (\fst x) (\fst y).
lemma segment_ordered_set_corefl:
- ∀O,s. coreflexive ? (wloss O ? (segment_ordered_set_exc O s)).
+ ∀O,s. coreflexive ? (wloss O ?? (segment_ordered_set_exc O s)).
intros 3; cases x; cases (wloss_prop O);
generalize in match (hos_coreflexive O w);
-rewrite < (H1 ? (segment_ordered_set_exc O s));
-rewrite < (H1 ? (hos_excess_ O)); intros; assumption;
+rewrite < (H1 ?? (segment_ordered_set_exc O s));
+rewrite < (H1 ?? (hos_excess_ O)); intros; assumption;
qed.
lemma segment_ordered_set_cotrans :
- ∀O,s. cotransitive ? (wloss O ? (segment_ordered_set_exc O s)).
+ ∀O,s. cotransitive ? (wloss O ?? (segment_ordered_set_exc O s)).
intros 5 (O s x y z); cases x; cases y ; cases z; clear x y z;
generalize in match (hos_cotransitive O w w1 w2);
cases (wloss_prop O);
-do 3 rewrite < (H3 ? (segment_ordered_set_exc O s));
-do 3 rewrite < (H3 ? (hos_excess_ O)); intros; apply H4; assumption;
+do 3 rewrite < (H3 ?? (segment_ordered_set_exc O s));
+do 3 rewrite < (H3 ?? (hos_excess_ O)); intros; apply H4; assumption;
qed.
lemma half_segment_ordered_set:
intros; try reflexivity;
*)
+lemma prove_in_segment:
+ ∀O:half_ordered_set.∀s:segment O.∀x:O.
+ (seg_l O s) ≤≤ x → x ≤≤ (seg_u O s) → x ∈ s.
+intros; unfold; cases (wloss_prop O); rewrite < H2;
+split; assumption;
+qed.
+
+lemma cases_in_segment:
+ ∀C:half_ordered_set.∀s:segment C.∀x. x ∈ s → (seg_l C s) ≤≤ x ∧ x ≤≤ (seg_u C s).
+intros; unfold in H; cases (wloss_prop C) (W W); rewrite<W in H; [cases H; split;assumption]
+cases H; split; assumption;
+qed.
+
definition hint_sequence:
∀C:ordered_set.
sequence (hos_carr (os_l C)) → sequence (Type_of_ordered_set C).
(* Lemma 2.9 - non easily dualizable *)
-lemma x2sx:
+lemma x2sx_:
∀O:half_ordered_set.
∀s:segment O.∀x,y:half_segment_ordered_set ? s.
\fst x ≰≰ \fst y → x ≰≰ y.
intros 4; cases x; cases y; clear x y; simplify; unfold hos_excess;
-whd in ⊢ (?→? (% ? ?) ? ? ? ?); simplify in ⊢ (?→%);
+whd in ⊢ (?→? (% ? ?)? ? ? ? ?); simplify in ⊢ (?→%);
cases (wloss_prop O) (E E); do 2 rewrite < E; intros; assumption;
qed.
-lemma sx2x:
+lemma sx2x_:
∀O:half_ordered_set.
∀s:segment O.∀x,y:half_segment_ordered_set ? s.
x ≰≰ y → \fst x ≰≰ \fst y.
intros 4; cases x; cases y; clear x y; simplify; unfold hos_excess;
-whd in ⊢ (? (% ? ?) ? ? ? ? → ?); simplify in ⊢ (% → ?);
+whd in ⊢ (? (% ? ?) ?? ? ? ? → ?); simplify in ⊢ (% → ?);
cases (wloss_prop O) (E E); do 2 rewrite < E; intros; assumption;
qed.
+lemma l2sl_:
+ ∀C,s.∀x,y:half_segment_ordered_set C s. \fst x ≤≤ \fst y → x ≤≤ y.
+intros; intro; apply H; apply sx2x_; apply H1;
+qed.
+
+
+lemma sl2l_:
+ ∀C,s.∀x,y:half_segment_ordered_set C s. x ≤≤ y → \fst x ≤≤ \fst y.
+intros; intro; apply H; apply x2sx_; apply H1;
+qed.
+
+coercion x2sx_ nocomposites.
+coercion sx2x_ nocomposites.
+coercion l2sl_ nocomposites.
+coercion sl2l_ nocomposites.
+
lemma h_segment_preserves_supremum:
∀O:half_ordered_set.∀s:segment O.
∀a:sequence (half_segment_ordered_set ? s).
supremum ? ⌊n,\fst (a n)⌋ (\fst x) → uparrow ? a x.
intros; split; cases H; clear H;
[1: intro n; lapply (H1 n) as K; clear H1 H2;
- intro; apply K; clear K; apply (sx2x ???? H);
+ intro; apply K; clear K; apply rule H;
|2: cases H2; split; clear H2;
[1: intro n; lapply (H n) as K; intro W; apply K;
- apply (sx2x ???? W);
+ apply rule W;
|2: clear H1 H; intros (y0 Hy0); cases (H3 (\fst y0));[exists[apply w]]
- [1: change in H with (\fst (a w) ≰≰ \fst y0); apply (x2sx ???? H);
- |2: apply (sx2x ???? Hy0);]]]
+ [1: change in H with (\fst (a w) ≰≰ \fst y0); apply rule H;
+ |2: apply rule Hy0;]]]
qed.
notation "'segment_preserves_supremum'" non associative with precedence 90 for @{'segment_preserves_supremum}.
*)
(* Definition 2.10 *)
+
alias symbol "pi2" = "pair pi2".
alias symbol "pi1" = "pair pi1".
+(*
definition square_segment ≝
λ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:half_ordered_set.λU:square_half_ordered_set O → Prop.
∀s.U s → le O (\fst s) (\snd s) →