---

Step * of Lemma truncate-rational_wf

∀q:ℚ. ∀e:{e:ℚ| 0 < e} .  (truncate-rational(q;e) ∈ ∃q':ℚ [(|q - q'| ≤ e)])
BY
{ (Auto THEN Subst' truncate-rational(q;e) ~ TERMOF{rational-truncate:o, \\v:l} q e 0 THEN Auto) }

1
.....equality..... 
1. q : ℚ
2. e : {e:ℚ| 0 < e} 
⊢ truncate-rational(q;e) ~ TERMOF{rational-truncate:o, \\v:l} q e

---

Latex:

---

Latex:
\mforall{}q:\mBbbQ{}.  \mforall{}e:\{e:\mBbbQ{}|  0  <  e\}  .    (truncate-rational(q;e)  \mmember{}  \mexists{}q':\mBbbQ{}  [(|q  -  q'|  \mleq{}  e)])


By

---

Latex:
(Auto  THEN  Subst'  truncate-rational(q;e)  \msim{}  TERMOF\{rational-truncate:o,  \mbackslash{}\mbackslash{}v:l\}  q  e  0  THEN  Auto)

---

Home Index