---

Step * of Lemma fset_for_when_eq

∀s:DSet. ∀g:IAbMonoid. ∀f:|s| ⟶ |g|. ∀e:|s|. ∀as:FiniteSet{s}.
  ((↑(e ∈b as)) ⇒ ((msFor{g} x ∈ as. when x (=b) e. f[x]) = f[e] ∈ |g|))
BY
{ ((RepD THENM RWH (LemmaWithC [`u',e] `fset_for_when_unique`) 0) THEN Auto) }

1
1. s : DSet
2. g : IAbMonoid
3. f : |s| ⟶ |g|
4. e : |s|
5. as : FiniteSet{s}
6. ↑(e
∈b as)
7. v : |s|
8. ↑(v (=b) e)
9. ↑(v
∈b as)
⊢ v = e ∈ |s|

---

Latex:

---

Latex:
\mforall{}s:DSet.  \mforall{}g:IAbMonoid.  \mforall{}f:|s|  {}\mrightarrow{}  |g|.  \mforall{}e:|s|.  \mforall{}as:FiniteSet\{s\}.
    ((\muparrow{}(e  \mmember{}\msubb{}  as))  {}\mRightarrow{}  ((msFor\{g\}  x  \mmember{}  as.  when  x  (=\msubb{})  e.  f[x])  =  f[e]))


By

---

Latex:
((RepD  THENM  RWH  (LemmaWithC  [`u',e]  `fset\_for\_when\_unique`)  0)  THEN  Auto)

---

Home Index