---

Step * 1 of Lemma truncate-rational-property


1. q : ℚ@i
2. e : {e:ℚ| 0 < e} @i
⊢ |q - truncate-rational(q;e)| ≤ e
BY
{ (GenConclTerm truncate-rational(q;e) ⋅ THENA Auto)⋅ }

1
1. q : ℚ@i
2. e : {e:ℚ| 0 < e} @i
3. v : ∃q':{ℚ| (|q - q'| ≤ e)}@i
4. truncate-rational(q;e) = v ∈ (∃q':{ℚ| (|q - q'| ≤ e)})@i
⊢ |q - v| ≤ e

---

Latex:

---

Latex:

1.  q  :  \mBbbQ{}@i
2.  e  :  \{e:\mBbbQ{}|  0  <  e\}  @i
\mvdash{}  |q  -  truncate-rational(q;e)|  \mleq{}  e


By

---

Latex:
(GenConclTerm  truncate-rational(q;e)  \mcdot{}  THENA  Auto)\mcdot{}

---

Home Index