Step
*
2
of Lemma
fabmon_of_nat_mcp_wf
1. s : DSet
2. m : MCopower(s;<ℤ+>↓hgrp)
3. g' : AbMon
4. f : |s| ⟶ |g'|
⊢ (((λm',f. (m.umap m' (λz,n. (nat(n) ⋅ (f z))))) g' f) o (λu.(m.inj u zhgrp(1)))) = f ∈ (|s| ⟶ |g'|)
BY
{ ((Ext THEN Reduce 0) THEN Auto) }
1
1. s : DSet
2. m : MCopower(s;<ℤ+>↓hgrp)
3. g' : AbMon
4. f : |s| ⟶ |g'|
5. x : |s|
⊢ (m.umap g' (λz,n. (nat(n) ⋅ (f z))) (m.inj x zhgrp(1))) = (f x) ∈ |g'|
Latex:
Latex:
1. s : DSet
2. m : MCopower(s;<\mBbbZ{}+>\mdownarrow{}hgrp)
3. g' : AbMon
4. f : |s| {}\mrightarrow{} |g'|
\mvdash{} (((\mlambda{}m',f. (m.umap m' (\mlambda{}z,n. (nat(n) \mcdot{} (f z))))) g' f) o (\mlambda{}u.(m.inj u zhgrp(1)))) = f
By
Latex:
((Ext THEN Reduce 0) THEN Auto)
Home
Index