---

Step * of Lemma real-interval-m-TB

∀a:ℝ. ∀b:{b:ℝ| a ≤ b} .  m-TB({x:ℝ| x ∈ [a, b]} ;rmetric())
BY
{ (Auto
   THEN (InstLemma `interval-totally-bounded` [⌜a⌝;⌜b⌝]⋅ THENA Auto)
   THEN (RWO "m-TB-iff" 0 THENA Auto)
   THEN (D 0 THENA Auto)
   THEN (D -2 With ⌜(r1/r(k + 1))⌝  THENA Auto)
   THEN (D -1 THENA Auto)
   THEN ParallelLast
   THEN ExRepD
   THEN RenameVar `xs' (-3)
   THEN All (RepUR ``rset-member mdist rmetric``)
   THEN D 0 With ⌜xs⌝ 
   THEN Auto) }

1
.....wf..... 
1. a : ℝ
2. b : {b:ℝ| a ≤ b} 
3. k : ℕ
4. n : ℕ+
5. xs : ℕn ⟶ ℝ
6. ∀i:ℕn. ((a ≤ (xs i)) ∧ ((xs i) ≤ b))
7. ∀x:ℝ. (((a ≤ x) ∧ (x ≤ b)) ⇒ (∃i:ℕn. (|x - xs i| < (r1/r(k + 1)))))
⊢ xs ∈ ℕn ⟶ {x:ℝ| (a ≤ x) ∧ (x ≤ b)} 

2
1. a : ℝ
2. b : {b:ℝ| a ≤ b} 
3. k : ℕ
4. n : ℕ+
5. xs : ℕn ⟶ ℝ
6. ∀i:ℕn. ((a ≤ (xs i)) ∧ ((xs i) ≤ b))
7. ∀x:ℝ. (((a ≤ x) ∧ (x ≤ b)) ⇒ (∃i:ℕn. (|x - xs i| < (r1/r(k + 1)))))
8. x : {x:ℝ| (a ≤ x) ∧ (x ≤ b)} 
⊢ ∃i:ℕn. (|x - xs i| ≤ (r1/r(k + 1)))

---

Latex:

---

Latex:
\mforall{}a:\mBbbR{}.  \mforall{}b:\{b:\mBbbR{}|  a  \mleq{}  b\}  .    m-TB(\{x:\mBbbR{}|  x  \mmember{}  [a,  b]\}  ;rmetric())


By

---

Latex:
(Auto
  THEN  (InstLemma  `interval-totally-bounded`  [\mkleeneopen{}a\mkleeneclose{};\mkleeneopen{}b\mkleeneclose{}]\mcdot{}  THENA  Auto)
  THEN  (RWO  "m-TB-iff"  0  THENA  Auto)
  THEN  (D  0  THENA  Auto)
  THEN  (D  -2  With  \mkleeneopen{}(r1/r(k  +  1))\mkleeneclose{}    THENA  Auto)
  THEN  (D  -1  THENA  Auto)
  THEN  ParallelLast
  THEN  ExRepD
  THEN  RenameVar  `xs'  (-3)
  THEN  All  (RepUR  ``rset-member  mdist  rmetric``)
  THEN  D  0  With  \mkleeneopen{}xs\mkleeneclose{} 
  THEN  Auto)

---

Home Index