---

Step * of Lemma increasing-baire-eq-from

∀a:ℕ ⟶ ℕ. ∀k:ℕ.  (increasing-sequence(a) ⇒ increasing-sequence(baire_eq_from(a;k)))
BY
{ ((UnivCD THENA Auto) THEN (D 0 THENA Auto) THEN RepUR ``baire_eq_from`` 0 THEN RepeatFor 2 (AutoSplit)) }

1
1. a : ℕ ⟶ ℕ
2. k : ℕ
3. increasing-sequence(a)
4. n : ℕ
5. ¬n + 1 < k
6. n < k
⊢ ((a k) = (a n) ∈ ℕ) ∨ ((a k) = ((a n) + 1) ∈ ℕ)

---

Latex:

---

Latex:
\mforall{}a:\mBbbN{}  {}\mrightarrow{}  \mBbbN{}.  \mforall{}k:\mBbbN{}.    (increasing-sequence(a)  {}\mRightarrow{}  increasing-sequence(baire\_eq\_from(a;k)))


By

---

Latex:
((UnivCD  THENA  Auto)
  THEN  (D  0  THENA  Auto)
  THEN  RepUR  ``baire\_eq\_from``  0
  THEN  RepeatFor  2  (AutoSplit))

---

Home Index