Step
*
1
1
of Lemma
oal_le_char
1. s : LOSet
2. g : OGrp
3. x : |oal(s;g)|
4. y : |oal(s;g)|
⊢ x ≤{s,g} y 
⇐⇒ (x = y ∈ |oal(s;g)|) ∨ (x << y)
BY
{ RepUnfolds ``oal_le oal_ble`` 0 }
1
1. s : LOSet
2. g : OGrp
3. x : |oal(s;g)|
4. y : |oal(s;g)|
⊢ ↑((x (=b) y) ∨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