Step
*
of Lemma
grp_le_wf
∀[g:GrpSig]. (≤b ∈ |g| ⟶ |g| ⟶ 𝔹)
BY
{ ModulePiTac 6 ``grp_car grp_eq grp_le grp_op grp_id grp_inv`` }
Latex:
Latex:
\mforall{}[g:GrpSig]. (\mleq{}\msubb{} \mmember{} |g| {}\mrightarrow{} |g| {}\mrightarrow{} \mBbbB{})
By
Latex:
ModulePiTac 6 ``grp\_car grp\_eq grp\_le grp\_op grp\_id grp\_inv``
Home
Index