---

Step * 1 1 1 2 of Lemma rational-truncate


1. q : ℚ
2. e : {e:ℚ| 0 < e} 
3. e < 1
4. v : ∀q:ℚ. ∀e:{e:ℚ| 0 < e ∧ e < 1} .  (∃p:ℤ × ℕ+ [((|q - (fst(p)/snd(p))| ≤ e) ∧ (((snd(p)) * e) ≤ 2))])
5. TERMOF{rational-truncate1:o, 1:l}
= v
∈ (∀q:ℚ. ∀e:{e:ℚ| 0 < e ∧ e < 1} .  (∃p:ℤ × ℕ+ [((|q - (fst(p)/snd(p))| ≤ e) ∧ (((snd(p)) * e) ≤ 2))]))
6. (v q e) = (v q e) ∈ (∃p:ℤ × ℕ+ [((|q - (fst(p)/snd(p))| ≤ e) ∧ (((snd(p)) * e) ≤ 2))])
⊢ (∃p:ℤ × ℕ+ [((|q - (fst(p)/snd(p))| ≤ e) ∧ (((snd(p)) * e) ≤ 2))]) ⊆r ℚ
BY
{ (All Thin
   THEN Using [`B',⌜ℤ × ℤ-o⌝] (BLemma `subtype_rel_transitivity`)⋅
   THEN Auto
   THEN Try ((D (-2) THEN Reduce 0 THEN Auto))
   THEN D 0
   THEN Auto) }

1
.....subterm..... T:t
1:n
1. q : ℚ
2. e : {e:ℚ| 0 < e} 
3. x : ℤ × ℤ-o
⊢ x ∈ ℚ

---

Latex:

---

Latex:

1.  q  :  \mBbbQ{}
2.  e  :  \{e:\mBbbQ{}|  0  <  e\} 
3.  e  <  1
4.  v  :  \mforall{}q:\mBbbQ{}.  \mforall{}e:\{e:\mBbbQ{}|  0  <  e  \mwedge{}  e  <  1\}  .
                  (\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\}  =  v
6.  (v  q  e)  =  (v  q  e)
\mvdash{}  (\mexists{}p:\mBbbZ{}  \mtimes{}  \mBbbN{}\msupplus{}  [((|q  -  (fst(p)/snd(p))|  \mleq{}  e)  \mwedge{}  (((snd(p))  *  e)  \mleq{}  2))])  \msubseteq{}r  \mBbbQ{}


By

---

Latex:
(All  Thin
  THEN  Using  [`B',\mkleeneopen{}\mBbbZ{}  \mtimes{}  \mBbbZ{}\msupminus{}\msupzero{}\mkleeneclose{}]  (BLemma  `subtype\_rel\_transitivity`)\mcdot{}
  THEN  Auto
  THEN  Try  ((D  (-2)  THEN  Reduce  0  THEN  Auto))
  THEN  D  0
  THEN  Auto)

---

Home Index