---

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


1. [k] : ℕ
2. c : ℚCube(k)
3. ∀i:ℕk. (↑Inhabited(c i))
⊢ ∃p:ℝ^k. in-rat-cube(k;p;c)
BY
{ ((D 0 With ⌜λi.rat2real(fst((c i)))⌝  THEN Auto) THEN D 0 THEN Reduce 0 THEN Try (Complete (Auto))) }

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

---

Latex:

---

Latex:

1.  [k]  :  \mBbbN{}
2.  c  :  \mBbbQ{}Cube(k)
3.  \mforall{}i:\mBbbN{}k.  (\muparrow{}Inhabited(c  i))
\mvdash{}  \mexists{}p:\mBbbR{}\^{}k.  in-rat-cube(k;p;c)


By

---

Latex:
((D  0  With  \mkleeneopen{}\mlambda{}i.rat2real(fst((c  i)))\mkleeneclose{}    THEN  Auto)  THEN  D  0  THEN  Reduce  0  THEN  Try  (Complete  (Auto)))

---

Home Index