---

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


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)))
BY
{ (Auto THEN InstLemma `iseg_member` [⌜ℤ⌝;⌜map(f;upto(i + 1))⌝;⌜map(f;upto(j + 1))⌝;⌜x⌝]⋅ THEN Auto) }

1
.....antecedent..... 
1. f : ℕ ⟶ ℤ@i
2. i : ℕ@i
3. j : ℕ@i
4. i ≤ j@i
5. x : ℤ@i
6. (x ∈ map(f;upto(i + 1)))@i
⊢ map(f;upto(i + 1)) ≤ 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
5.  x  :  \mBbbZ{}@i
\mvdash{}  (x  \mmember{}  map(f;upto(i  +  1)))  {}\mRightarrow{}  (x  \mmember{}  map(f;upto(j  +  1)))


By

---

Latex:
(Auto  THEN  InstLemma  `iseg\_member`  [\mkleeneopen{}\mBbbZ{}\mkleeneclose{};\mkleeneopen{}map(f;upto(i  +  1))\mkleeneclose{};\mkleeneopen{}map(f;upto(j  +  1))\mkleeneclose{};\mkleeneopen{}x\mkleeneclose{}]\mcdot{}  THEN  Auto)

---

Home Index