---

Step * of Lemma truncate-rational-property

∀q:ℚ. ∀e:{e:ℚ| 0 < e} .  ((|q - truncate-rational(q;e)| ≤ e) ∧ (|truncate-rational(q;e) - q| ≤ e))
BY
{ Auto }

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

---

Latex:

---

Latex:
\mforall{}q:\mBbbQ{}.  \mforall{}e:\{e:\mBbbQ{}|  0  <  e\}  .    ((|q  -  truncate-rational(q;e)|  \mleq{}  e)  \mwedge{}  (|truncate-rational(q;e)  -  q|  \mleq{}  e))


By

---

Latex:
Auto

---

Home Index