---

Step * of Lemma q-linear_wf

∀[k:ℕ]. ∀[X:ℕ ⟶ ℚ]. ∀[y:ℚ List].  q-linear(k;j.X[j];y) ∈ ℚ supposing k ≤ ||y||
BY
{ (Unfold `q-linear` 0 THEN Auto) }

---

Latex:

---

Latex:
\mforall{}[k:\mBbbN{}].  \mforall{}[X:\mBbbN{}  {}\mrightarrow{}  \mBbbQ{}].  \mforall{}[y:\mBbbQ{}  List].    q-linear(k;j.X[j];y)  \mmember{}  \mBbbQ{}  supposing  k  \mleq{}  ||y||


By

---

Latex:
(Unfold  `q-linear`  0  THEN  Auto)

---

Home Index