---

Step * 1 of Lemma increasing-sequence-prop1


1. n : ℕ
2. k : ℕ
3. a : ℕ ⟶ ℕ
4. increasing-sequence(a)
5. n ≤ (n + k)
⊢ (a n) ≤ (a (n + k))
BY
{ (Thin (-1)⋅ THEN NatInd 2 THEN Auto) }

1
.....upcase..... 
1. n : ℕ
2. a : ℕ ⟶ ℕ
3. increasing-sequence(a)
4. k : ℤ
5. 0 < k
6. (a n) ≤ (a (n + (k - 1)))
⊢ (a n) ≤ (a (n + k))

---

Latex:

---

Latex:

1.  n  :  \mBbbN{}
2.  k  :  \mBbbN{}
3.  a  :  \mBbbN{}  {}\mrightarrow{}  \mBbbN{}
4.  increasing-sequence(a)
5.  n  \mleq{}  (n  +  k)
\mvdash{}  (a  n)  \mleq{}  (a  (n  +  k))


By

---

Latex:
(Thin  (-1)\mcdot{}  THEN  NatInd  2  THEN  Auto)

---

Home Index