Step
*
1
1
of Lemma
oal_le_is_order
1. s : LOSet@i'
2. g : OGrp@i'
⊢ order(|oal(s;g)|;x,y:|oal(s;g)|. x ≤{s,g} y)
BY
{ (((RWW "oal_le_char" 0) THENA Auto) THEN Try (Try ((BLemma `ocgrp_abdgrp` THEN Auto)))) }
1
1. s : LOSet@i'
2. g : OGrp@i'
⊢ order(|oal(s;g)|;(x,y:|oal(s;g)|. x << y)o)
Latex:
Latex:
1. s : LOSet@i'
2. g : OGrp@i'
\mvdash{} order(|oal(s;g)|;x,y:|oal(s;g)|. x \mleq{}\{s,g\} y)
By
Latex:
(((RWW "oal\_le\_char" 0) THENA Auto) THEN Try (Try ((BLemma `ocgrp\_abdgrp` THEN Auto))))
Home
Index