---

Step * of Lemma imax-list-lb

∀[L:ℤ List]. ∀[a:ℤ].  uiff(imax-list(L) ≤ a;(∀b∈L.b ≤ a)) supposing 0 < ||L||
BY
{ (Assert Assoc(ℤ;λx,y. imax(x;y)) BY
         (D 0 THEN Reduce 0 THEN Auto)) }

1
1. Assoc(ℤ;λx,y. imax(x;y))
⊢ ∀[L:ℤ List]. ∀[a:ℤ].  uiff(imax-list(L) ≤ a;(∀b∈L.b ≤ a)) supposing 0 < ||L||

---

Latex:

---

Latex:
\mforall{}[L:\mBbbZ{}  List].  \mforall{}[a:\mBbbZ{}].    uiff(imax-list(L)  \mleq{}  a;(\mforall{}b\mmember{}L.b  \mleq{}  a))  supposing  0  <  ||L||


By

---

Latex:
(Assert  Assoc(\mBbbZ{};\mlambda{}x,y.  imax(x;y))  BY
              (D  0  THEN  Reduce  0  THEN  Auto))

---

Home Index