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`` 
THENM GenRepD THENA Auto) }

1
1. DSet@i'
2. |s|@i
3. a1 MSet{s}
4. a2 MSet{s}
⊢ x ∈b a1 a2 (x ∈b a1) ∨b(x ∈b a2)

2
1. DSet@i'
2. |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