---

Step * 2 2 1 of Lemma rational-truncate


1. q : ℚ
2. e : {e:ℚ| 0 < e} 
3. ¬e < 1
4. v : ℚ
5. 0 ≤ v
6. v < 1
7. fractional-part(q) = v ∈ {r:ℚ| (0 ≤ r) ∧ r < 1} 
⊢ |v| ≤ e
BY
{ (RWO "qless_complement_qorder" 3 THEN Auto) }

1
1. q : ℚ
2. e : {e:ℚ| 0 < e} 
3. 1 ≤ e
4. v : ℚ
5. 0 ≤ v
6. v < 1
7. fractional-part(q) = v ∈ {r:ℚ| (0 ≤ r) ∧ r < 1} 
⊢ |v| ≤ e

---

Latex:

---

Latex:

1.  q  :  \mBbbQ{}
2.  e  :  \{e:\mBbbQ{}|  0  <  e\} 
3.  \mneg{}e  <  1
4.  v  :  \mBbbQ{}
5.  0  \mleq{}  v
6.  v  <  1
7.  fractional-part(q)  =  v
\mvdash{}  |v|  \mleq{}  e


By

---

Latex:
(RWO  "qless\_complement\_qorder"  3  THEN  Auto)

---

Home Index