---

Step * 1 of Lemma qtruncate-property


1. q : ℚ
2. N : ℕ+
3. q-ceil(q * N) - 1 < q * N ∧ ((q * N) ≤ q-ceil(q * N))
⊢ qtruncate(q;N) - (1/N) < q ∧ (q ≤ qtruncate(q;N))
BY
{ (Unfold `qtruncate` 0 THEN Auto THEN (QMul ⌜N⌝ 0⋅ THENA Auto) THEN QNorm (-2) THEN Auto) }

---

Latex:

---

Latex:

1.  q  :  \mBbbQ{}
2.  N  :  \mBbbN{}\msupplus{}
3.  q-ceil(q  *  N)  -  1  <  q  *  N  \mwedge{}  ((q  *  N)  \mleq{}  q-ceil(q  *  N))
\mvdash{}  qtruncate(q;N)  -  (1/N)  <  q  \mwedge{}  (q  \mleq{}  qtruncate(q;N))


By

---

Latex:
(Unfold  `qtruncate`  0  THEN  Auto  THEN  (QMul  \mkleeneopen{}N\mkleeneclose{}  0\mcdot{}  THENA  Auto)  THEN  QNorm  (-2)  THEN  Auto)

---

Home Index