---

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


1. f : ℕ ⟶ ℤ@i
2. ∀i,j:ℕ.  ((i ≤ j) ⇒ (imax-list(map(f;upto(i + 1))) ≤ imax-list(map(f;upto(j + 1)))))
3. n : ℕ@i
⊢ (f n) ≤ imax-list(map(f;upto(n + 1)))
BY
{ (RWW "imax-list-ub" 0⋅
   THEN Auto
   THEN RWW "map-length length_upto" 0⋅
   THEN Auto
   THEN (BLemma `l_exists_iff` THENA Auto)
   THEN ((With ⌜f n⌝ (D 0)⋅ THEN Auto)
         THEN GenListD 0
         THEN Auto
         THEN With ⌜n⌝ (D 0)⋅
         THEN Auto
         THEN GenListD 0
         THEN Auto)⋅) }

---

Latex:

---

Latex:

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


By

---

Latex:
(RWW  "imax-list-ub"  0\mcdot{}
  THEN  Auto
  THEN  RWW  "map-length  length\_upto"  0\mcdot{}
  THEN  Auto
  THEN  (BLemma  `l\_exists\_iff`  THENA  Auto)
  THEN  ((With  \mkleeneopen{}f  n\mkleeneclose{}  (D  0)\mcdot{}  THEN  Auto)
              THEN  GenListD  0
              THEN  Auto
              THEN  With  \mkleeneopen{}n\mkleeneclose{}  (D  0)\mcdot{}
              THEN  Auto
              THEN  GenListD  0
              THEN  Auto)\mcdot{})

---

Home Index