---

Step * of Lemma tuple_wf_ntuple

∀[n:ℕ]. ∀[F:Top].  (tuple(n;i.F[i]) ∈ n-tuple(n))
BY
{ (((InductionOnNat THEN RWO "n-tuple-decomp tuple-decomp" 0) THENA Auto) THEN Reduce 0 THEN Auto) }

---

Latex:

---

Latex:
\mforall{}[n:\mBbbN{}].  \mforall{}[F:Top].    (tuple(n;i.F[i])  \mmember{}  n-tuple(n))


By

---

Latex:
(((InductionOnNat  THEN  RWO  "n-tuple-decomp  tuple-decomp"  0)  THENA  Auto)  THEN  Reduce  0  THEN  Auto)

---

Home Index