---

Step * 3 of Lemma qmax-list-bounds


1. L : ℚ List
2. 0 < ||L||
3. x : ℚ
⊢ qmax-list(L) < x ⇐⇒ (∀y∈L.y < x)
BY
{ (((InstLemma `combine-list-rel-and` [⌜ℚ⌝;⌜λ2x y.qmax(x;y)⌝;⌜λ2x y.y < x⌝;⌜L⌝;⌜x⌝]⋅ THENA Try (Complete (Auto)))
   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. qmax(y;z) < x1
⊢ y < x1

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

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

4
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{}  qmax-list(L)  <  x  \mLeftarrow{}{}\mRightarrow{}  (\mforall{}y\mmember{}L.y  <  x)


By

---

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

---

Home Index