seg_u_ : O
}.
-notation > "đŚ_term 90 s" non associative with precedence 45 for @{'upp $s}.
-notation "đŚ \sub term 90 s" non associative with precedence 45 for @{'upp $s}.
-notation > "đ_term 90 s" non associative with precedence 45 for @{'low $s}.
-notation "đ \sub term 90 s" non associative with precedence 45 for @{'low $s}.
+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.
(* 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.
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.
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}.