---

Step * of Lemma qmax-list-unique

∀[L:ℚ List]. ∀[a:ℚ].  uiff(qmax-list(L) = a ∈ ℚ;(∀b∈L.b ≤ a)) supposing (a ∈ L)
BY
{ (InstLemma `qmax-list-bounds` []
   THEN ParallelLast'
   THEN RepeatFor 2 ((D 0 THENA Auto))
   THEN (D (-3) THENA Auto)
   THEN (InstHyp [⌜a⌝] (-1)⋅ THENA Auto)
   THEN Thin (-2)
   THEN (Assert 0 < ||L|| BY
               Auto)
   THEN Auto
   THEN ThinTrivial⋅
   THEN Try ((BackThruSomeHyp THEN RelRST THEN Auto)⋅)
   THEN (Assert (∃y∈L. a ≤ y) BY
               (D 3 THEN With ⌜i⌝ (D 0)⋅ THEN Auto))
   THEN ThinTrivial
   THEN Try ((RelRST THEN Auto))) }

---

Latex:

---

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


By

---

Latex:
(InstLemma  `qmax-list-bounds`  []
  THEN  ParallelLast'
  THEN  RepeatFor  2  ((D  0  THENA  Auto))
  THEN  (D  (-3)  THENA  Auto)
  THEN  (InstHyp  [\mkleeneopen{}a\mkleeneclose{}]  (-1)\mcdot{}  THENA  Auto)
  THEN  Thin  (-2)
  THEN  (Assert  0  <  ||L||  BY
                          Auto)
  THEN  Auto
  THEN  ThinTrivial\mcdot{}
  THEN  Try  ((BackThruSomeHyp  THEN  RelRST  THEN  Auto)\mcdot{})
  THEN  (Assert  (\mexists{}y\mmember{}L.  a  \mleq{}  y)  BY
                          (D  3  THEN  With  \mkleeneopen{}i\mkleeneclose{}  (D  0)\mcdot{}  THEN  Auto))
  THEN  ThinTrivial
  THEN  Try  ((RelRST  THEN  Auto)))

---

Home Index