---

Step * of Lemma integer-part-decomp

∀q:ℚ. (∃p:{ℤ × {r:ℚ| (0 ≤ r) ∧ r < 1} | let x,r = p in q = (x + r) ∈ ℚ})
BY
{ (Auto THEN UseWitness ⌜rat-int-part(q)⌝⋅ THEN Auto) }

---

Latex:

---

Latex:
\mforall{}q:\mBbbQ{}.  (\mexists{}p:\{\mBbbZ{}  \mtimes{}  \{r:\mBbbQ{}|  (0  \mleq{}  r)  \mwedge{}  r  <  1\}  |  let  x,r  =  p  in  q  =  (x  +  r)\})


By

---

Latex:
(Auto  THEN  UseWitness  \mkleeneopen{}rat-int-part(q)\mkleeneclose{}\mcdot{}  THEN  Auto)

---

Home Index