---

Step * 1 of Lemma make-strict-agrees


1. alpha : ℕ ⟶ ℕ
2. n : ℕ
⊢ strictly-increasing-seq(n;alpha) ⇒ (∀i:ℕn. ((make-strict(alpha) i) = (alpha i) ∈ ℤ))
BY
{ (NatInd (-1) THEN Auto THEN (D -3 THENA RepeatFor 2 (ParallelOp -2))) }

1
1. alpha : ℕ ⟶ ℕ
2. n : ℤ
3. 0 < n
4. strictly-increasing-seq(n;alpha)
5. i : ℕn
6. ∀i:ℕn - 1. ((make-strict(alpha) i) = (alpha i) ∈ ℤ)
⊢ (make-strict(alpha) i) = (alpha i) ∈ ℤ

---

Latex:

---

Latex:

1.  alpha  :  \mBbbN{}  {}\mrightarrow{}  \mBbbN{}
2.  n  :  \mBbbN{}
\mvdash{}  strictly-increasing-seq(n;alpha)  {}\mRightarrow{}  (\mforall{}i:\mBbbN{}n.  ((make-strict(alpha)  i)  =  (alpha  i)))


By

---

Latex:
(NatInd  (-1)  THEN  Auto  THEN  (D  -3  THENA  RepeatFor  2  (ParallelOp  -2)))

---

Home Index