---

Step * 2 1 1 of Lemma mcompact-rat-cube

.....aux..... 
1. k : ℕ
2. c : ℚCube(k)
3. ↑Inhabited(c)
4. mcompact(i:ℕk ⟶ {x:ℝ| x ∈ [rat2real(fst((c i))), rat2real(snd((c i)))]} ;rn-prod-metric(k))
5. x : i:ℕk ⟶ {x:ℝ| x ∈ [rat2real(fst((c i))), rat2real(snd((c i)))]} 
⊢ in-rat-cube(k;x;c)
BY
{ ((D 0 THENW Auto) THEN (GenConclTerm ⌜x i⌝⋅ THENA Auto) THEN All Reduce THEN Auto) }

---

Latex:

---

Latex:
.....aux..... 
1.  k  :  \mBbbN{}
2.  c  :  \mBbbQ{}Cube(k)
3.  \muparrow{}Inhabited(c)
4.  mcompact(i:\mBbbN{}k  {}\mrightarrow{}  \{x:\mBbbR{}|  x  \mmember{}  [rat2real(fst((c  i))),  rat2real(snd((c  i)))]\}  ;rn-prod-metric(k))
5.  x  :  i:\mBbbN{}k  {}\mrightarrow{}  \{x:\mBbbR{}|  x  \mmember{}  [rat2real(fst((c  i))),  rat2real(snd((c  i)))]\} 
\mvdash{}  in-rat-cube(k;x;c)


By

---

Latex:
((D  0  THENW  Auto)  THEN  (GenConclTerm  \mkleeneopen{}x  i\mkleeneclose{}\mcdot{}  THENA  Auto)  THEN  All  Reduce  THEN  Auto)

---

Home Index