---

Step * of Lemma imax-list-unique

∀[L:ℤ List]. ∀[a:ℤ].  uiff(imax-list(L) = a ∈ ℤ;(∀b∈L.b ≤ a)) supposing (a ∈ L)
BY
{ (InstLemma `imax-list-lb` []
   THEN RepeatFor 2 (ParallelLast')
   THEN (D 0 THENA Auto)
   THEN (Assert 0 < ||L|| BY
               ((DVar `L' THEN All Reduce THEN Auto') THEN AutoSimpHyp Auto (-1)))
   THEN ThinTrivial
   THEN InstLemma `imax-list-ub` [⌜L⌝;⌜a⌝]⋅
   THEN Auto
   THEN ThinTrivial) }

1
1. L : ℤ List
2. a : ℤ
3. (a ∈ L)
4. 0 < ||L||
5. (a ≤ imax-list(L)) ⇒ (∃b∈L. a ≤ b)
6. (a ≤ imax-list(L)) ⇐ (∃b∈L. a ≤ b)
7. (∀b∈L.b ≤ a)
8. imax-list(L) ≤ a
9. (∀b∈L.b ≤ a)
⊢ imax-list(L) = a ∈ ℤ

---

Latex:

---

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


By

---

Latex:
(InstLemma  `imax-list-lb`  []
  THEN  RepeatFor  2  (ParallelLast')
  THEN  (D  0  THENA  Auto)
  THEN  (Assert  0  <  ||L||  BY
                          ((DVar  `L'  THEN  All  Reduce  THEN  Auto')  THEN  AutoSimpHyp  Auto  (-1)))
  THEN  ThinTrivial
  THEN  InstLemma  `imax-list-ub`  [\mkleeneopen{}L\mkleeneclose{};\mkleeneopen{}a\mkleeneclose{}]\mcdot{}
  THEN  Auto
  THEN  ThinTrivial)

---

Home Index