Step
*
1
of Lemma
omral_fact_a
∀g:OCMon. ∀r:CDRng. ∀ps:|omral(g;r)|. (ps = (msFor{oal_mon(g↓oset;r↓+gp)} k' ∈ dom(ps). inj(k',ps[k'])) ∈ |omral(g;r)|)
BY
{ Lemma `omral_fact` }
Latex:
Latex:
\mforall{}g:OCMon. \mforall{}r:CDRng. \mforall{}ps:|omral(g;r)|.
(ps = (msFor\{oal\_mon(g\mdownarrow{}oset;r\mdownarrow{}+gp)\} k' \mmember{} dom(ps). inj(k',ps[k'])))
By
Latex:
Lemma `omral\_fact`
Home
Index