---

Step * 2 1 1 1 of Lemma rational-truncate


1. q : ℚ
2. e : {e:ℚ| 0 < e} 
3. e < 1
4. v1 : ℤ
5. v2 : ℕ+
6. (|q - (fst(<v1, v2>)/snd(<v1, v2>))| ≤ e) ∧ (((snd(<v1, v2>)) * e) ≤ 2)
7. (TERMOF{rational-truncate1:o, 1:l} q e)
= <v1, v2>
∈ (∃p:ℤ × ℕ+ [((|q - (fst(p)/snd(p))| ≤ e) ∧ (((snd(p)) * e) ≤ 2))])
⊢ |q - <v1, v2>| ≤ e
BY
{ (All Reduce THEN Auto) }

---

Latex:

---

Latex:

1.  q  :  \mBbbQ{}
2.  e  :  \{e:\mBbbQ{}|  0  <  e\} 
3.  e  <  1
4.  v1  :  \mBbbZ{}
5.  v2  :  \mBbbN{}\msupplus{}
6.  (|q  -  (fst(<v1,  v2>)/snd(<v1,  v2>))|  \mleq{}  e)  \mwedge{}  (((snd(<v1,  v2>))  *  e)  \mleq{}  2)
7.  (TERMOF\{rational-truncate1:o,  1:l\}  q  e)  =  <v1,  v2>
\mvdash{}  |q  -  <v1,  v2>|  \mleq{}  e


By

---

Latex:
(All  Reduce  THEN  Auto)

---

Home Index