---

Step * of Lemma min-increasing-sequence-prop1

∀b:ℕ ⟶ ℕ. ∀n,x,k:ℕ.  ((min-increasing-sequence(b;n;x) = (inl k) ∈ (ℕ?)) ⇒ (x ≤ (b k)))
BY
{ (RepeatFor 2 ((D 0 THENA Auto)) THEN NatInd (-1) THEN (UnivCD THENA Auto)) }

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

2
1. b : ℕ ⟶ ℕ
2. n : ℤ
3. 0 < n
4. ∀x,k:ℕ.  ((min-increasing-sequence(b;n - 1;x) = (inl k) ∈ (ℕ?)) ⇒ (x ≤ (b k)))
5. x : ℕ
6. k : ℕ
7. min-increasing-sequence(b;n;x) = (inl k) ∈ (ℕ?)
⊢ x ≤ (b k)

---

Latex:

---

Latex:
\mforall{}b:\mBbbN{}  {}\mrightarrow{}  \mBbbN{}.  \mforall{}n,x,k:\mBbbN{}.    ((min-increasing-sequence(b;n;x)  =  (inl  k))  {}\mRightarrow{}  (x  \mleq{}  (b  k)))


By

---

Latex:
(RepeatFor  2  ((D  0  THENA  Auto))  THEN  NatInd  (-1)  THEN  (UnivCD  THENA  Auto))

---

Home Index