---

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

No Annotations
∀[k:ℕ]. ∀c:ℚCube(k). uiff(↑Inhabited(c);∃x:ℕk ⟶ ℚ. rat-point-in-cube(k;x;c))
BY
{ ((RWO "assert-inhabited-rat-cube" 0 THENA Auto) THEN Unfold `rat-point-in-cube` 0 THEN Auto THEN ExRepD) }

1
1. [k] : ℕ
2. c : ℚCube(k)
3. ∀i:ℕk. (↑Inhabited(c i))
⊢ ∃x:ℕk ⟶ ℚ. ∀i:ℕk. (((fst((c i))) ≤ (x i)) ∧ ((x i) ≤ (snd((c i)))))

2
1. k : ℕ
2. c : ℚCube(k)
3. x : ℕk ⟶ ℚ
4. ∀i:ℕk. (((fst((c i))) ≤ (x i)) ∧ ((x i) ≤ (snd((c i)))))
5. i : ℕk
⊢ ↑Inhabited(c i)

---

Latex:

---

Latex:
No  Annotations
\mforall{}[k:\mBbbN{}].  \mforall{}c:\mBbbQ{}Cube(k).  uiff(\muparrow{}Inhabited(c);\mexists{}x:\mBbbN{}k  {}\mrightarrow{}  \mBbbQ{}.  rat-point-in-cube(k;x;c))


By

---

Latex:
((RWO  "assert-inhabited-rat-cube"  0  THENA  Auto)
  THEN  Unfold  `rat-point-in-cube`  0
  THEN  Auto
  THEN  ExRepD)

---

Home Index