---

Step * of Lemma rational-truncate

∀q:ℚ. ∀e:{e:ℚ| 0 < e} .  (∃q':ℚ [(|q - q'| ≤ e)])
BY
{ (Auto THEN With ⌜if q_less(e;1) then TERMOF{rational-truncate1:o, 1:l} q e else integer-part(q) fi ⌝ (D 0)⋅) }

1
.....wf..... 
1. q : ℚ
2. e : {e:ℚ| 0 < e} 
⊢ if q_less(e;1) then TERMOF{rational-truncate1:o, 1:l} q e else integer-part(q) fi  ∈ ℚ

2
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

3
.....wf..... 
1. q : ℚ
2. e : {e:ℚ| 0 < e} 
3. q' : ℚ
⊢ |q - q'| ≤ e ∈ ℙ

---

Latex:

---

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


By

---

Latex:
(Auto
  THEN  With  \mkleeneopen{}if  q\_less(e;1)  then  TERMOF\{rational-truncate1:o,  1:l\}  q  e  else  integer-part(q)  fi  \mkleeneclose{}
              (D  0)\mcdot{}
  )

---

Home Index