---

Step * 1 1 of Lemma truncate-rational-property


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
BY
{ (DVar `v' THEN Unhide THEN Auto) }

---

Latex:

---

Latex:

1.  q  :  \mBbbQ{}@i
2.  e  :  \{e:\mBbbQ{}|  0  <  e\}  @i
3.  v  :  \mexists{}q':\{\mBbbQ{}|  (|q  -  q'|  \mleq{}  e)\}@i
4.  truncate-rational(q;e)  =  v@i
\mvdash{}  |q  -  v|  \mleq{}  e


By

---

Latex:
(DVar  `v'  THEN  Unhide  THEN  Auto)

---

Home Index