---

Step * of Lemma inhabited-iff-in-rat-cube

∀[k:ℕ]. ∀c:ℚCube(k). (↑Inhabited(c) ⇐⇒ ∃p:ℝ^k. in-rat-cube(k;p;c))
BY
{ (Auto THEN (All (RWO "assert-inhabited-rat-cube") THENA Auto)) }

1
1. [k] : ℕ
2. c : ℚCube(k)
3. ∀i:ℕk. (↑Inhabited(c i))
⊢ ∃p:ℝ^k. in-rat-cube(k;p;c)

2
1. k : ℕ
2. c : ℚCube(k)
3. ∃p:ℝ^k. in-rat-cube(k;p;c)
⊢ ∀i:ℕk. (↑Inhabited(c i))

---

Latex:

---

Latex:
\mforall{}[k:\mBbbN{}].  \mforall{}c:\mBbbQ{}Cube(k).  (\muparrow{}Inhabited(c)  \mLeftarrow{}{}\mRightarrow{}  \mexists{}p:\mBbbR{}\^{}k.  in-rat-cube(k;p;c))


By

---

Latex:
(Auto  THEN  (All  (RWO  "assert-inhabited-rat-cube")  THENA  Auto))

---

Home Index