---

Step * 2 1 of Lemma mcompact-rat-cube


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))
⊢ mcompact({x:ℝ^k| in-rat-cube(k;x;c)} ;rn-prod-metric(k))
BY
{ ((Assert i:ℕk ⟶ {x:ℝ| x ∈ [rat2real(fst((c i))), rat2real(snd((c i)))]}  ≡ {x:ℝ^k| in-rat-cube(k;x;c)}  BY
          ((RepeatFor 2 (D 0) THENA Auto)
           THEN DSetVars
           THEN (((FunExt THENM D -2 With ⌜i⌝ ) THEN Auto) ORELSE (MemTypeCD THEN Auto))))
THENM (RWO "-1" (-2) THEN Auto)
) }

1
.....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)

---

Latex:

---

Latex:

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))
\mvdash{}  mcompact(\{x:\mBbbR{}\^{}k|  in-rat-cube(k;x;c)\}  ;rn-prod-metric(k))


By

---

Latex:
((Assert  i:\mBbbN{}k  {}\mrightarrow{}  \{x:\mBbbR{}|  x  \mmember{}  [rat2real(fst((c  i))),  rat2real(snd((c  i)))]\}    \mequiv{}  \{x:\mBbbR{}\^{}k| 
                                                                                                                                                        in-rat-cube(k;x;c)\}    BY
                ((RepeatFor  2  (D  0)  THENA  Auto)
                  THEN  DSetVars
                  THEN  (((FunExt  THENM  D  -2  With  \mkleeneopen{}i\mkleeneclose{}  )  THEN  Auto)  ORELSE  (MemTypeCD  THEN  Auto))))
THENM  (RWO  "-1"  (-2)  THEN  Auto)
)

---

Home Index