Step * 2 1 1 of Lemma rational-truncate


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

1
1. : ℚ
2. {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} e)
= <v1, v2>
∈ (∃p:ℤ × ℕ+ [((|q (fst(p)/snd(p))| ≤ e) ∧ (((snd(p)) e) ≤ 2))])
⊢ |q - <v1, v2>| ≤ e


Latex:


Latex:

1.  q  :  \mBbbQ{}
2.  e  :  \{e:\mBbbQ{}|  0  <  e\} 
3.  e  <  1
4.  v  :  \mexists{}p:\mBbbZ{}  \mtimes{}  \mBbbN{}\msupplus{}  [((|q  -  (fst(p)/snd(p))|  \mleq{}  e)  \mwedge{}  (((snd(p))  *  e)  \mleq{}  2))]
5.  (TERMOF\{rational-truncate1:o,  1:l\}  q  e)  =  v
\mvdash{}  |q  -  v|  \mleq{}  e


By


Latex:
(((D  (-2)  THEN  D  -3)  THEN  Unhide)  THENA  Auto)




Home Index