Step * 3 of Lemma qmax-list-bounds


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

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

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

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

4
1. : ℚ List
2. 0 < ||L||
3. : ℚ
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