---

Step * of Lemma member-fset-image

∀[T,A:Type]. ∀[eqt:EqDecider(T)]. ∀[eqa:EqDecider(A)]. ∀[f:T ⟶ A]. ∀[s:fset(T)]. ∀[x:T].  f x ∈ f"(s) supposing x ∈ s
BY
{ (Auto THEN (BLemma `member-fset-image-iff` THEN Auto)⋅) }

---

Latex:

---

Latex:
\mforall{}[T,A:Type].  \mforall{}[eqt:EqDecider(T)].  \mforall{}[eqa:EqDecider(A)].  \mforall{}[f:T  {}\mrightarrow{}  A].  \mforall{}[s:fset(T)].  \mforall{}[x:T].
    f  x  \mmember{}  f"(s)  supposing  x  \mmember{}  s


By

---

Latex:
(Auto  THEN  (BLemma  `member-fset-image-iff`  THEN  Auto)\mcdot{})

---

Home Index