---

Step * 3 of Lemma qmin-list-bounds


1. L : ℚ List
2. 0 < ||L||
3. x : ℚ
⊢ x < qmin-list(L) ⇐⇒ (∀y∈L.x < y)
BY
{ ((InstLemma `combine-list-rel-and`
            [⌜ℚ⌝;⌜λ2x y.qmin(x;y)⌝;⌜λ2x y.x < y⌝;⌜L⌝;⌜x⌝]⋅
   THENM (Fold `qmin-list` (-1) THEN NthHyp (-1))
   )
   THEN Auto
   THEN All (Unfold `qmin`)⋅
   THEN Try ((SplitOnHypITE -1  THENA Auto))
   THEN RWW "qle_complement_qorder" (-1)
   THEN Auto) }

---

Latex:

---

Latex:

1.  L  :  \mBbbQ{}  List
2.  0  <  ||L||
3.  x  :  \mBbbQ{}
\mvdash{}  x  <  qmin-list(L)  \mLeftarrow{}{}\mRightarrow{}  (\mforall{}y\mmember{}L.x  <  y)


By

---

Latex:
((InstLemma  `combine-list-rel-and`
                    [\mkleeneopen{}\mBbbQ{}\mkleeneclose{};\mkleeneopen{}\mlambda{}\msubtwo{}x  y.qmin(x;y)\mkleeneclose{};\mkleeneopen{}\mlambda{}\msubtwo{}x  y.x  <  y\mkleeneclose{};\mkleeneopen{}L\mkleeneclose{};\mkleeneopen{}x\mkleeneclose{}]\mcdot{}
  THENM  (Fold  `qmin-list`  (-1)  THEN  NthHyp  (-1))
  )
  THEN  Auto
  THEN  All  (Unfold  `qmin`)\mcdot{}
  THEN  Try  ((SplitOnHypITE  -1    THENA  Auto))
  THEN  RWW  "qle\_complement\_qorder"  (-1)
  THEN  Auto)

---

Home Index