Step
*
of Lemma
mset_sum_bor_mon_hom
∀s:DSet. ∀x:|s|. IsMonHom{mset_mon{s},<𝔹,∨b>}(λu.(x ∈b u))
BY
{ ((Eval ``monoid_hom_p fun_thru_2op`` 0
THENM GenRepD ) THENA Auto) }
1
1. s : DSet@i'
2. x : |s|@i
3. a1 : MSet{s}
4. a2 : MSet{s}
⊢ x ∈b a1 + a2 = (x ∈b a1) ∨b(x ∈b a2)
2
1. s : DSet@i'
2. x : |s|@i
⊢ ff = ff
Latex:
Latex:
\mforall{}s:DSet. \mforall{}x:|s|. IsMonHom\{mset\_mon\{s\},<\mBbbB{},\mvee{}\msubb{}>\}(\mlambda{}u.(x \mmember{}\msubb{} u))
By
Latex:
((Eval ``monoid\_hom\_p fun\_thru\_2op`` 0
THENM GenRepD ) THENA Auto)
Home
Index