---

Step * 4 of Lemma qmax-list-bounds


1. L : ℚ List
2. 0 < ||L||
3. x : ℚ
⊢ x < qmax-list(L) ⇐⇒ (∃y∈L. x < y)
BY
{ ((InstLemma `combine-list-rel-or` [⌜ℚ⌝;⌜λ2x y.qmax(x;y)⌝;⌜λ2x y.x < y⌝;⌜L⌝;⌜x⌝]⋅
   THENM (Fold `qmax-list` (-1) THEN NthHyp (-1))
   )
   THEN Auto
   ) }

1
1. L : ℚ List
2. 0 < ||L||
3. x : ℚ
4. x1 : ℚ
5. y : ℚ
6. z : ℚ
7. x1 < qmax(y;z)
⊢ x1 < y ∨ x1 < z

2
1. L : ℚ List
2. 0 < ||L||
3. x : ℚ
4. x1 : ℚ
5. y : ℚ
6. z : ℚ
7. x1 < y ∨ x1 < z
⊢ x1 < qmax(y;z)

3
1. L : ℚ List
2. 0 < ||L||
3. x : ℚ
4. 0 < ||L||
⊢ Assoc(ℚ;λx,y. qmax(x;y))

---

Latex:

---

Latex:

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


By

---

Latex:
((InstLemma  `combine-list-rel-or`  [\mkleeneopen{}\mBbbQ{}\mkleeneclose{};\mkleeneopen{}\mlambda{}\msubtwo{}x  y.qmax(x;y)\mkleeneclose{};\mkleeneopen{}\mlambda{}\msubtwo{}x  y.x  <  y\mkleeneclose{};\mkleeneopen{}L\mkleeneclose{};\mkleeneopen{}x\mkleeneclose{}]\mcdot{}
  THENM  (Fold  `qmax-list`  (-1)  THEN  NthHyp  (-1))
  )
  THEN  Auto
  )

---

Home Index