---

Step * of Lemma implies-strictly-increasing-seq

∀[n:ℕ]. ∀[s:ℕn ⟶ ℤ].  ((∀i:ℕn - 1. s i < s (i + 1)) ⇒ strictly-increasing-seq(n;s))
BY
{ (Auto THEN UnfoldTopAb 0 THEN Assert ⌜∀d:ℕ. ∀j:ℕn. ∀i:ℕj.  (((j - i) ≤ d) ⇒ s i < s j)⌝⋅) }

1
.....assertion..... 
1. n : ℕ
2. s : ℕn ⟶ ℤ
3. ∀i:ℕn - 1. s i < s (i + 1)
⊢ ∀d:ℕ. ∀j:ℕn. ∀i:ℕj.  (((j - i) ≤ d) ⇒ s i < s j)

2
1. n : ℕ
2. s : ℕn ⟶ ℤ
3. ∀i:ℕn - 1. s i < s (i + 1)
4. ∀d:ℕ. ∀j:ℕn. ∀i:ℕj.  (((j - i) ≤ d) ⇒ s i < s j)
⊢ ∀j:ℕn. ∀i:ℕj.  s i < s j

---

Latex:

---

Latex:
\mforall{}[n:\mBbbN{}].  \mforall{}[s:\mBbbN{}n  {}\mrightarrow{}  \mBbbZ{}].    ((\mforall{}i:\mBbbN{}n  -  1.  s  i  <  s  (i  +  1))  {}\mRightarrow{}  strictly-increasing-seq(n;s))


By

---

Latex:
(Auto  THEN  UnfoldTopAb  0  THEN  Assert  \mkleeneopen{}\mforall{}d:\mBbbN{}.  \mforall{}j:\mBbbN{}n.  \mforall{}i:\mBbbN{}j.    (((j  -  i)  \mleq{}  d)  {}\mRightarrow{}  s  i  <  s  j)\mkleeneclose{}\mcdot{})

---

Home Index