---

Step * of Lemma assert_of_oal_blt

∀s:LOSet. ∀g:OGrp. ∀ps,qs:|oal(s;g)|.  (↑(ps <<b qs) ⇐⇒ ps << qs)
BY
{ TACTIC:((UnivCD THENA Auto) THEN Unfold `oal_lt` 0) }

1
1. s : LOSet
2. g : OGrp
3. ps : |oal(s;g)|
4. qs : |oal(s;g)|
⊢ ↑(ps <<b qs) ⇐⇒ ∃k:|s|. ((∀k':|s|. ((k <s k') ⇒ ((ps[k']) = (qs[k']) ∈ |g|))) ∧ ((ps[k]) < (qs[k])))

---

Latex:

---

Latex:
\mforall{}s:LOSet.  \mforall{}g:OGrp.  \mforall{}ps,qs:|oal(s;g)|.    (\muparrow{}(ps  <<\msubb{}  qs)  \mLeftarrow{}{}\mRightarrow{}  ps  <<  qs)


By

---

Latex:
TACTIC:((UnivCD  THENA  Auto)  THEN  Unfold  `oal\_lt`  0)

---

Home Index