---

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