---

Step * of Lemma member-eclass-iff-size1

∀[Info,T:Type]. ∀[X:EClass(T)]. ∀[es:EO+(Info)]. ∀[e:E].  (↑e ∈b X ⇐⇒ 1 ≤ #(X es e))
BY
{ ((UnivCD THENA Auto) THEN RWO "member-eclass-iff-size" 0 THEN Auto) }

---

Latex:


\mforall{}[Info,T:Type].  \mforall{}[X:EClass(T)].  \mforall{}[es:EO+(Info)].  \mforall{}[e:E].    (\muparrow{}e  \mmember{}\msubb{}  X  \mLeftarrow{}{}\mRightarrow{}  1  \mleq{}  \#(X  es  e))


By

((UnivCD  THENA  Auto)  THEN  RWO  "member-eclass-iff-size"  0  THEN  Auto)

---

Home Index