---

Step * of Lemma setmem-mk-set

∀T:Type. ∀f:T ⟶ Set{i:l}. ∀t:T.  (f t ∈ f"(T))
BY
{ (Auto THEN BLemma `setmem-iff` THEN Auto THEN Reduce 0 THEN D 0 With ⌜t⌝  THEN Auto) }

---

Latex:

---

Latex:
\mforall{}T:Type.  \mforall{}f:T  {}\mrightarrow{}  Set\{i:l\}.  \mforall{}t:T.    (f  t  \mmember{}  f"(T))


By

---

Latex:
(Auto  THEN  BLemma  `setmem-iff`  THEN  Auto  THEN  Reduce  0  THEN  D  0  With  \mkleeneopen{}t\mkleeneclose{}    THEN  Auto)

---

Home Index