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