---

Step * of Lemma ranked-eo-E

∀[L:Id ─→ (Top List)]. ∀[rk:Top]. ∀[e:i:Id × ℕ||L i||].  (e ∈ E)
BY
{ (RepUR ``ranked-eo es-E mk-extended-eo mk-eo mk-eo-record`` 0 THEN Auto) }

---

Latex:

---

Latex:
\mforall{}[L:Id  {}\mrightarrow{}  (Top  List)].  \mforall{}[rk:Top].  \mforall{}[e:i:Id  \mtimes{}  \mBbbN{}||L  i||].    (e  \mmember{}  E)


By

---

Latex:
(RepUR  ``ranked-eo  es-E  mk-extended-eo  mk-eo  mk-eo-record``  0  THEN  Auto)

---

Home Index