---

Step * of Lemma real-vec-infinity-norm_wf

No Annotations
∀[n:ℕ+]. ∀[v:ℝ^n].  (||v||∞ ∈ ℝ)
BY
{ (Auto THEN (Assert λi.r0 ∈ ℝ^n BY Auto) THEN ProveWfLemma) }

---

Latex:

---

Latex:
No  Annotations
\mforall{}[n:\mBbbN{}\msupplus{}].  \mforall{}[v:\mBbbR{}\^{}n].    (||v||\minfty{}  \mmember{}  \mBbbR{})


By

---

Latex:
(Auto  THEN  (Assert  \mlambda{}i.r0  \mmember{}  \mBbbR{}\^{}n  BY  Auto)  THEN  ProveWfLemma)

---

Home Index