---

Step * 1 1 1 of Lemma oal_lt_iff_grp_lt


1. s : LOSet@i'
2. g : OGrp@i'
3. ps : |oal(s;g)|@i
4. qs : |oal(s;g)|@i
⊢ ps [x,y:|oal(s;g)|. x << y] qs ⇐⇒ (ps ≤ qs) ∧ (¬(qs ≤ ps))
BY
{ (((RWW "oal_lt_char" 0) THENA Auto) THEN Try ((BLemma `ocgrp_abdgrp` THEN Auto))) }

1
1. s : LOSet@i'
2. g : OGrp@i'
3. ps : |oal(s;g)|@i
4. qs : |oal(s;g)|@i
⊢ ps [(x,y:|oal(s;g)|. x ≤{s,g} y)\] qs ⇐⇒ (ps ≤ qs) ∧ (¬(qs ≤ ps))

---

Latex:

---

Latex:

1.  s  :  LOSet@i'
2.  g  :  OGrp@i'
3.  ps  :  |oal(s;g)|@i
4.  qs  :  |oal(s;g)|@i
\mvdash{}  ps  [x,y:|oal(s;g)|.  x  <<  y]  qs  \mLeftarrow{}{}\mRightarrow{}  (ps  \mleq{}  qs)  \mwedge{}  (\mneg{}(qs  \mleq{}  ps))


By

---

Latex:
(((RWW  "oal\_lt\_char"  0)  THENA  Auto)  THEN  Try  ((BLemma  `ocgrp\_abdgrp`  THEN  Auto)))

---

Home Index