Step * of Lemma grp_le_wf

[g:GrpSig]. (≤b ∈ |g| ⟶ |g| ⟶ 𝔹)
BY
ModulePiTac ``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