---

Step * of Lemma make-strict-agrees

∀[alpha:ℕ ⟶ ℕ]. ∀[n:ℕ].  ∀[i:ℕn]. ((make-strict(alpha) i) = (alpha i) ∈ ℤ) supposing strictly-increasing-seq(n;alpha)
BY
{ (Auto THEN RepeatFor 2 (MoveToConcl (-1))) }

1
1. alpha : ℕ ⟶ ℕ
2. n : ℕ
⊢ strictly-increasing-seq(n;alpha) ⇒ (∀i:ℕn. ((make-strict(alpha) i) = (alpha i) ∈ ℤ))

---

Latex:

---

Latex:
\mforall{}[alpha:\mBbbN{}  {}\mrightarrow{}  \mBbbN{}].  \mforall{}[n:\mBbbN{}].
    \mforall{}[i:\mBbbN{}n].  ((make-strict(alpha)  i)  =  (alpha  i))  supposing  strictly-increasing-seq(n;alpha)


By

---

Latex:
(Auto  THEN  RepeatFor  2  (MoveToConcl  (-1)))

---

Home Index