---

Step * of Lemma stable__real-vec-indep

∀[k:ℕ]. ∀[L:ℝ^k List].  Stable{real-vec-indep(k;L)}
BY
{ (Unfold `real-vec-indep` 0 THEN Auto) }

1
1. k : ℕ
2. L : ℝ^k List
⊢ Stable{∀a:ℕ||L|| ⟶ ℝ. (req-vec(k;Σ{a i*L[i] | 0≤i≤||L|| - 1};λi.r0) ⇒ (∀i:ℕ||L||. ((a i) = r0)))}

---

Latex:

---

Latex:
\mforall{}[k:\mBbbN{}].  \mforall{}[L:\mBbbR{}\^{}k  List].    Stable\{real-vec-indep(k;L)\}


By

---

Latex:
(Unfold  `real-vec-indep`  0  THEN  Auto)

---

Home Index