---

Step * of Lemma rcolumn_wf

∀[n:ℕ]. ∀[b:ℝ^n].  (col(b) ∈ ℝ(n × 1))
BY
{ (RepUR ``real-vec rmatrix`` 0 THEN ProveWfLemma) }

---

Latex:

---

Latex:
\mforall{}[n:\mBbbN{}].  \mforall{}[b:\mBbbR{}\^{}n].    (col(b)  \mmember{}  \mBbbR{}(n  \mtimes{}  1))


By

---

Latex:
(RepUR  ``real-vec  rmatrix``  0  THEN  ProveWfLemma)

---

Home Index