Step
*
of Lemma
eqv_mod_subset_wf
∀[g:GrpSig]. ∀[s:|g| ⟶ ℙ]. ∀[a,b:|g|]. (a ≡ b (mod s in g) ∈ ℙ)
BY
{ Unfold `eqv_mod_subset` 0 THEN Auto }
Latex:
Latex:
\mforall{}[g:GrpSig]. \mforall{}[s:|g| {}\mrightarrow{} \mBbbP{}]. \mforall{}[a,b:|g|]. (a \mequiv{} b (mod s in g) \mmember{} \mBbbP{})
By
Latex:
Unfold `eqv\_mod\_subset` 0 THEN Auto
Home
Index