---

Step * 1 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 skip{Auto}
   ) }

1
.....antecedent..... 
1. L : ℚ List
2. 0 < ||L||
3. x : ℚ
⊢ ∀x,y,z:ℚ.  (qmax(y;z) ≤ x ⇐⇒ (y ≤ x) ∧ (z ≤ x))

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

---

Latex:

---

Latex:

1.  L  :  \mBbbQ{}  List
2.  0  <  ||L||
3.  x  :  \mBbbQ{}
\mvdash{}  qmax-list(L)  \mleq{}  x  \mLeftarrow{}{}\mRightarrow{}  (\mforall{}y\mmember{}L.y  \mleq{}  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  \mleq{}  x\mkleeneclose{};\mkleeneopen{}L\mkleeneclose{};\mkleeneopen{}x\mkleeneclose{}]\mcdot{}
      THENA  Try  (Complete  (Auto))
      )
  THENM  (Fold  `qmax-list`  (-1)  THEN  NthHyp  (-1))
  )
  THEN  skip\{Auto\}
  )

---

Home Index