Step * 1 1 of Lemma oal_le_char


1. LOSet
2. OGrp
3. |oal(s;g)|
4. |oal(s;g)|
⊢ x ≤{s,g} ⇐⇒ (x y ∈ |oal(s;g)|) ∨ (x << y)
BY
RepUnfolds ``oal_le oal_ble`` }

1
1. LOSet
2. OGrp
3. |oal(s;g)|
4. |oal(s;g)|
⊢ ↑((x (=by) ∨b(x <<b y)) ⇐⇒ (x y ∈ |oal(s;g)|) ∨ (x << y)


Latex:


Latex:

1.  s  :  LOSet
2.  g  :  OGrp
3.  x  :  |oal(s;g)|
4.  y  :  |oal(s;g)|
\mvdash{}  x  \mleq{}\{s,g\}  y  \mLeftarrow{}{}\mRightarrow{}  (x  =  y)  \mvee{}  (x  <<  y)


By


Latex:
RepUnfolds  ``oal\_le  oal\_ble``  0




Home Index