---

Step * of Lemma imax-list-unique2

∀L:ℤ List. ∀a:ℤ.  uiff((||L|| > 0) ∧ (imax-list(L) = a ∈ ℤ);(∀b∈L.b ≤ a) ∧ (a ∈ L))
BY
{ ((UnivCD THENA Auto)
   THEN D 0
   THEN (D 0 THENA Auto)
   THEN Auto
   THEN Try ((BLemma `imax-list-unique` THEN Auto))
   THEN BLemma `imax-list-eq-implies`
   THEN Auto) }

---

Latex:

---

Latex:
\mforall{}L:\mBbbZ{}  List.  \mforall{}a:\mBbbZ{}.    uiff((||L||  >  0)  \mwedge{}  (imax-list(L)  =  a);(\mforall{}b\mmember{}L.b  \mleq{}  a)  \mwedge{}  (a  \mmember{}  L))


By

---

Latex:
((UnivCD  THENA  Auto)
  THEN  D  0
  THEN  (D  0  THENA  Auto)
  THEN  Auto
  THEN  Try  ((BLemma  `imax-list-unique`  THEN  Auto))
  THEN  BLemma  `imax-list-eq-implies`
  THEN  Auto)

---

Home Index