---

Step * of Lemma setmem-coset

∀T:Type. ∀f:T ⟶ coSet{i:l}. ∀t:T.  (f t ∈ mk-coset(T;f))
BY
{ (Auto THEN RWO  "setmem-mk-coset" 0 THEN Auto) }

---

Latex:

---

Latex:
\mforall{}T:Type.  \mforall{}f:T  {}\mrightarrow{}  coSet\{i:l\}.  \mforall{}t:T.    (f  t  \mmember{}  mk-coset(T;f))


By

---

Latex:
(Auto  THEN  RWO    "setmem-mk-coset"  0  THEN  Auto)

---

Home Index