---

Step * of Lemma realvec-max-ibs_wf

∀[n:ℕ]. ∀[p:ℝ^n].  (realvec-max-ibs(n;p) ∈ IBS)
BY
{ (Auto THEN (Assert λi.r0 ∈ ℝ^n BY Auto) THEN ProveWfLemma) }

---

Latex:

---

Latex:
\mforall{}[n:\mBbbN{}].  \mforall{}[p:\mBbbR{}\^{}n].    (realvec-max-ibs(n;p)  \mmember{}  IBS)


By

---

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

---

Home Index