---

Step * 2 of Lemma rational-truncate


1. q : ℚ
2. e : {e:ℚ| 0 < e} 
⊢ |q - if q_less(e;1) then TERMOF{rational-truncate1:o, 1:l} q e else integer-part(q) fi | ≤ e
BY
{ (BoolCase ⌜q_less(e;1)⌝⋅ THENA Auto)⋅ }

1
1. q : ℚ
2. e : {e:ℚ| 0 < e} 
3. e < 1
⊢ |q - TERMOF{rational-truncate1:o, 1:l} q e| ≤ e

2
1. q : ℚ
2. e : {e:ℚ| 0 < e} 
3. ¬e < 1
⊢ |q - integer-part(q)| ≤ e

---

Latex:

---

Latex:

1.  q  :  \mBbbQ{}
2.  e  :  \{e:\mBbbQ{}|  0  <  e\} 
\mvdash{}  |q  -  if  q\_less(e;1)  then  TERMOF\{rational-truncate1:o,  1:l\}  q  e  else  integer-part(q)  fi  |  \mleq{}  e


By

---

Latex:
(BoolCase  \mkleeneopen{}q\_less(e;1)\mkleeneclose{}\mcdot{}  THENA  Auto)\mcdot{}

---

Home Index