---

Step * 1 of Lemma strict-inc-subtype


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

1
.....set predicate..... 
1. m : ℕ@i
2. x : ℕ ⟶ ℕ@i
3. ∀j:ℕ. ∀i:ℕj.  x i < x j@i
⊢ strictly-increasing-seq(m;x)

---

Latex:

---

Latex:

1.  m  :  \mBbbN{}@i
2.  x  :  \mBbbN{}  {}\mrightarrow{}  \mBbbN{}@i
3.  \mforall{}j:\mBbbN{}.  \mforall{}i:\mBbbN{}j.    x  i  <  x  j@i
\mvdash{}  x  \mmember{}  \{s:\mBbbN{}m  {}\mrightarrow{}  \mBbbN{}|  strictly-increasing-seq(m;s)\} 


By

---

Latex:
(MemTypeCD  THEN  Auto)

---

Home Index