---

Step * of Lemma canon-bnd_wf

∀[x:ℝ]. (canon-bnd(x) ∈ {k:{3...}| ∀n:ℕ+. (|x n| ≤ (n * k))} )
BY
{ ((D 0 THENA Auto) THEN D 1 THEN Unfold `canon-bnd` 0 THEN MemTypeCD THEN Auto) }

1
1. x : ℕ+ ⟶ ℤ
2. regular-seq(x)
3. n : ℕ+
⊢ |x n| ≤ (n * (|x 1| + 3))

---

Latex:

---

Latex:
\mforall{}[x:\mBbbR{}].  (canon-bnd(x)  \mmember{}  \{k:\{3...\}|  \mforall{}n:\mBbbN{}\msupplus{}.  (|x  n|  \mleq{}  (n  *  k))\}  )


By

---

Latex:
((D  0  THENA  Auto)  THEN  D  1  THEN  Unfold  `canon-bnd`  0  THEN  MemTypeCD  THEN  Auto)

---

Home Index