---

Step * of Lemma near-real-implies-real

∀[x:ℕ+ ⟶ ℤ]. ∀[y:ℝ].  x ∈ {x:ℝ| x = y}  supposing ∀n:ℕ+. (|(x within 1/n) - y| ≤ (r1/r(n)))
BY
{ (Auto THEN ExRepD THEN (Assert x ∈ ℝ BY (BLemma `implies-real` THEN Auto))) }

1
1. x : ℕ+ ⟶ ℤ
2. y : ℝ
3. ∀n:ℕ+. (|(x within 1/n) - y| ≤ (r1/r(n)))
4. n : ℕ+
5. m : ℕ+
⊢ |(x within 1/n) - (x within 1/m)| ≤ ((r1/r(n)) + (r1/r(m)))

2
1. x : ℕ+ ⟶ ℤ
2. y : ℝ
3. ∀n:ℕ+. (|(x within 1/n) - y| ≤ (r1/r(n)))
4. x ∈ ℝ
⊢ x ∈ {x:ℝ| x = y} 

---

Latex:

---

Latex:
\mforall{}[x:\mBbbN{}\msupplus{}  {}\mrightarrow{}  \mBbbZ{}].  \mforall{}[y:\mBbbR{}].    x  \mmember{}  \{x:\mBbbR{}|  x  =  y\}    supposing  \mforall{}n:\mBbbN{}\msupplus{}.  (|(x  within  1/n)  -  y|  \mleq{}  (r1/r(n)))


By

---

Latex:
(Auto  THEN  ExRepD  THEN  (Assert  x  \mmember{}  \mBbbR{}  BY  (BLemma  `implies-real`  THEN  Auto)))

---

Home Index