---

Step * 2 1 1 2 1 1 1 1 of Lemma interval-totally-bounded


1. e : ℝ
2. r0 < e
3. x : ℝ
4. k : ℤ
5. [%2] : 0 < k
6. ∀f:ℕ(k - 1) + 1 ⟶ ℝ
     (0 < k - 1
     ⇒ (∀i:ℕk - 1. (((f i) < (f (i + 1))) ∧ ((f (i + 1)) < ((f i) + e))))
     ⇒ (∀i:ℕk - 1. (((f i) < x) ∨ (x < (f (i + 1)))))
     ⇒ (x ≤ (f (k - 1)))
     ⇒ ((f 0) ≤ x)
     ⇒ (∃i:ℕ(k - 1) + 1. (|x - f i| < e)))
7. f : ℕk + 1 ⟶ ℝ
8. 0 < k
9. ∀i:ℕk. (((f i) < (f (i + 1))) ∧ ((f (i + 1)) < ((f i) + e)))
10. ∀i:ℕk. (((f i) < x) ∨ (x < (f (i + 1))))
11. x ≤ (f k)
12. (f 0) ≤ x
⊢ ∃i:ℕk + 1. (|x - f i| < e)
BY
{ ((InstHyp [⌜k - 1⌝] (-3)⋅ THENA Auto) THEN D -1) }

1
1. e : ℝ
2. r0 < e
3. x : ℝ
4. k : ℤ
5. [%2] : 0 < k
6. ∀f:ℕ(k - 1) + 1 ⟶ ℝ
     (0 < k - 1
     ⇒ (∀i:ℕk - 1. (((f i) < (f (i + 1))) ∧ ((f (i + 1)) < ((f i) + e))))
     ⇒ (∀i:ℕk - 1. (((f i) < x) ∨ (x < (f (i + 1)))))
     ⇒ (x ≤ (f (k - 1)))
     ⇒ ((f 0) ≤ x)
     ⇒ (∃i:ℕ(k - 1) + 1. (|x - f i| < e)))
7. f : ℕk + 1 ⟶ ℝ
8. 0 < k
9. ∀i:ℕk. (((f i) < (f (i + 1))) ∧ ((f (i + 1)) < ((f i) + e)))
10. ∀i:ℕk. (((f i) < x) ∨ (x < (f (i + 1))))
11. x ≤ (f k)
12. (f 0) ≤ x
13. (f (k - 1)) < x
⊢ ∃i:ℕk + 1. (|x - f i| < e)

2
1. e : ℝ
2. r0 < e
3. x : ℝ
4. k : ℤ
5. [%2] : 0 < k
6. ∀f:ℕ(k - 1) + 1 ⟶ ℝ
     (0 < k - 1
     ⇒ (∀i:ℕk - 1. (((f i) < (f (i + 1))) ∧ ((f (i + 1)) < ((f i) + e))))
     ⇒ (∀i:ℕk - 1. (((f i) < x) ∨ (x < (f (i + 1)))))
     ⇒ (x ≤ (f (k - 1)))
     ⇒ ((f 0) ≤ x)
     ⇒ (∃i:ℕ(k - 1) + 1. (|x - f i| < e)))
7. f : ℕk + 1 ⟶ ℝ
8. 0 < k
9. ∀i:ℕk. (((f i) < (f (i + 1))) ∧ ((f (i + 1)) < ((f i) + e)))
10. ∀i:ℕk. (((f i) < x) ∨ (x < (f (i + 1))))
11. x ≤ (f k)
12. (f 0) ≤ x
13. x < (f ((k - 1) + 1))
⊢ ∃i:ℕk + 1. (|x - f i| < e)

---

Latex:

---

Latex:

1.  e  :  \mBbbR{}
2.  r0  <  e
3.  x  :  \mBbbR{}
4.  k  :  \mBbbZ{}
5.  [\%2]  :  0  <  k
6.  \mforall{}f:\mBbbN{}(k  -  1)  +  1  {}\mrightarrow{}  \mBbbR{}
          (0  <  k  -  1
          {}\mRightarrow{}  (\mforall{}i:\mBbbN{}k  -  1.  (((f  i)  <  (f  (i  +  1)))  \mwedge{}  ((f  (i  +  1))  <  ((f  i)  +  e))))
          {}\mRightarrow{}  (\mforall{}i:\mBbbN{}k  -  1.  (((f  i)  <  x)  \mvee{}  (x  <  (f  (i  +  1)))))
          {}\mRightarrow{}  (x  \mleq{}  (f  (k  -  1)))
          {}\mRightarrow{}  ((f  0)  \mleq{}  x)
          {}\mRightarrow{}  (\mexists{}i:\mBbbN{}(k  -  1)  +  1.  (|x  -  f  i|  <  e)))
7.  f  :  \mBbbN{}k  +  1  {}\mrightarrow{}  \mBbbR{}
8.  0  <  k
9.  \mforall{}i:\mBbbN{}k.  (((f  i)  <  (f  (i  +  1)))  \mwedge{}  ((f  (i  +  1))  <  ((f  i)  +  e)))
10.  \mforall{}i:\mBbbN{}k.  (((f  i)  <  x)  \mvee{}  (x  <  (f  (i  +  1))))
11.  x  \mleq{}  (f  k)
12.  (f  0)  \mleq{}  x
\mvdash{}  \mexists{}i:\mBbbN{}k  +  1.  (|x  -  f  i|  <  e)


By

---

Latex:
((InstHyp  [\mkleeneopen{}k  -  1\mkleeneclose{}]  (-3)\mcdot{}  THENA  Auto)  THEN  D  -1)

---

Home Index