---

Step * of Lemma mtb-seq_wf

∀[X:Type]. ∀[d:metric(X)]. ∀[mtb:m-TB(X;d)]. ∀[s:mtb-cantor(mtb)].  (mtb-seq(mtb;s) ∈ ℕ ⟶ X)
BY
{ (Intros
   THEN Unhide
   THEN RepeatFor 2 (DVar `mtb')
   THEN D -3
   THEN Thin (-2)
   THEN All (RepUR ``mtb-cantor mtb-seq``)
   THEN Auto) }

---

Latex:

---

Latex:
\mforall{}[X:Type].  \mforall{}[d:metric(X)].  \mforall{}[mtb:m-TB(X;d)].  \mforall{}[s:mtb-cantor(mtb)].    (mtb-seq(mtb;s)  \mmember{}  \mBbbN{}  {}\mrightarrow{}  X)


By

---

Latex:
(Intros
  THEN  Unhide
  THEN  RepeatFor  2  (DVar  `mtb')
  THEN  D  -3
  THEN  Thin  (-2)
  THEN  All  (RepUR  ``mtb-cantor  mtb-seq``)
  THEN  Auto)

---

Home Index