---

Step * 1 1 of Lemma qmax-list-bounds

.....antecedent..... 
1. L : ℚ List
2. 0 < ||L||
3. x : ℚ
⊢ ∀x,y,z:ℚ.  (qmax(y;z) ≤ x ⇐⇒ (y ≤ x) ∧ (z ≤ x))
BY
{ 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

---

Latex:

---

Latex:
.....antecedent..... 
1.  L  :  \mBbbQ{}  List
2.  0  <  ||L||
3.  x  :  \mBbbQ{}
\mvdash{}  \mforall{}x,y,z:\mBbbQ{}.    (qmax(y;z)  \mleq{}  x  \mLeftarrow{}{}\mRightarrow{}  (y  \mleq{}  x)  \mwedge{}  (z  \mleq{}  x))


By

---

Latex:
Auto

---

Home Index