---

Step * of Lemma strict-inc-subtype

∀m:ℕ. (StrictInc ⊆r {s:ℕm ⟶ ℕ| strictly-increasing-seq(m;s)} )
BY
{ (Auto THEN (D 0 THENA Auto) THEN D -1) }

1
1. m : ℕ@i
2. x : ℕ ⟶ ℕ@i
3. ∀j:ℕ. ∀i:ℕj.  x i < x j@i
⊢ x ∈ {s:ℕm ⟶ ℕ| strictly-increasing-seq(m;s)} 

---

Latex:

---

Latex:
\mforall{}m:\mBbbN{}.  (StrictInc  \msubseteq{}r  \{s:\mBbbN{}m  {}\mrightarrow{}  \mBbbN{}|  strictly-increasing-seq(m;s)\}  )


By

---

Latex:
(Auto  THEN  (D  0  THENA  Auto)  THEN  D  -1)

---

Home Index