---

Step * 1 of Lemma monotone-upper-bound-function


1. f : ℕ ⟶ ℤ@i
2. i : ℕ@i
3. j : ℕ@i
4. i ≤ j@i
⊢ imax-list(map(f;upto(i + 1))) ≤ imax-list(map(f;upto(j + 1)))
BY
{ (BLemma `imax-list-subset` THEN Auto THEN RWW "map-length length_upto" 0⋅ THEN Auto THEN (D 0 THENA Auto)) }

1
1. f : ℕ ⟶ ℤ@i
2. i : ℕ@i
3. j : ℕ@i
4. i ≤ j@i
5. x : ℤ@i
⊢ (x ∈ map(f;upto(i + 1))) ⇒ (x ∈ map(f;upto(j + 1)))

---

Latex:

---

Latex:

1.  f  :  \mBbbN{}  {}\mrightarrow{}  \mBbbZ{}@i
2.  i  :  \mBbbN{}@i
3.  j  :  \mBbbN{}@i
4.  i  \mleq{}  j@i
\mvdash{}  imax-list(map(f;upto(i  +  1)))  \mleq{}  imax-list(map(f;upto(j  +  1)))


By

---

Latex:
(BLemma  `imax-list-subset`
  THEN  Auto
  THEN  RWW  "map-length  length\_upto"  0\mcdot{}
  THEN  Auto
  THEN  (D  0  THENA  Auto))

---

Home Index