---

Step * 2 1 of Lemma rational-truncate


1. q : ℚ
2. e : {e:ℚ| 0 < e} 
3. e < 1
⊢ |q - TERMOF{rational-truncate1:o, 1:l} q e| ≤ e
BY
{ GenConclAtAddr [1;1;2]⋅ }

1
1. q : ℚ
2. e : {e:ℚ| 0 < e} 
3. e < 1
4. v : ∃p:ℤ × ℕ+ [((|q - (fst(p)/snd(p))| ≤ e) ∧ (((snd(p)) * e) ≤ 2))]
5. (TERMOF{rational-truncate1:o, 1:l} q e) = v ∈ (∃p:ℤ × ℕ+ [((|q - (fst(p)/snd(p))| ≤ e) ∧ (((snd(p)) * e) ≤ 2))])
⊢ |q - v| ≤ e

---

Latex:

---

Latex:

1.  q  :  \mBbbQ{}
2.  e  :  \{e:\mBbbQ{}|  0  <  e\} 
3.  e  <  1
\mvdash{}  |q  -  TERMOF\{rational-truncate1:o,  1:l\}  q  e|  \mleq{}  e


By

---

Latex:
GenConclAtAddr  [1;1;2]\mcdot{}

---

Home Index