---

Step * of Lemma setmem-mk-coset

∀[T,f,x:Top].  ((x ∈ mk-coset(T;f)) ~ ∃t:T. seteq(x;f t))
BY
{ (RepUR ``setmem mk-coset coWmem coW-dom coW-item seteq`` 0 THEN Auto) }

---

Latex:

---

Latex:
\mforall{}[T,f,x:Top].    ((x  \mmember{}  mk-coset(T;f))  \msim{}  \mexists{}t:T.  seteq(x;f  t))


By

---

Latex:
(RepUR  ``setmem  mk-coset  coWmem  coW-dom  coW-item  seteq``  0  THEN  Auto)

---

Home Index