---

Step * 1 of Lemma min-increasing-sequence-prop1


1. b : ℕ ⟶ ℕ
2. n : ℤ
3. x : ℕ
4. k : ℕ
5. min-increasing-sequence(b;0;x) = (inl k) ∈ (ℕ?)
⊢ x ≤ (b k)
BY
{ (RepUR ``min-increasing-sequence`` (-1) THEN Auto) }

---

Latex:

---

Latex:

1.  b  :  \mBbbN{}  {}\mrightarrow{}  \mBbbN{}
2.  n  :  \mBbbZ{}
3.  x  :  \mBbbN{}
4.  k  :  \mBbbN{}
5.  min-increasing-sequence(b;0;x)  =  (inl  k)
\mvdash{}  x  \mleq{}  (b  k)


By

---

Latex:
(RepUR  ``min-increasing-sequence``  (-1)  THEN  Auto)

---

Home Index