---

Step * of Lemma qmax-list-bounds

No Annotations
∀L:ℚ List
  (0 < ||L||
  ⇒ (∀x:ℚ
        ((qmax-list(L) ≤ x ⇐⇒ (∀y∈L.y ≤ x))
        ∧ (x ≤ qmax-list(L) ⇐⇒ (∃y∈L. x ≤ y))
        ∧ (qmax-list(L) < x ⇐⇒ (∀y∈L.y < x))
        ∧ (x < qmax-list(L) ⇐⇒ (∃y∈L. x < y)))))
BY
{ (RepeatFor 3 ((D 0 THENA Auto)) THEN SplitAndConcl) }

1
1. L : ℚ List
2. 0 < ||L||
3. x : ℚ
⊢ qmax-list(L) ≤ x ⇐⇒ (∀y∈L.y ≤ x)

2
1. L : ℚ List
2. 0 < ||L||
3. x : ℚ
⊢ x ≤ qmax-list(L) ⇐⇒ (∃y∈L. x ≤ y)

3
1. L : ℚ List
2. 0 < ||L||
3. x : ℚ
⊢ qmax-list(L) < x ⇐⇒ (∀y∈L.y < x)

4
1. L : ℚ List
2. 0 < ||L||
3. x : ℚ
⊢ x < qmax-list(L) ⇐⇒ (∃y∈L. x < y)

---

Latex:

---

Latex:
No  Annotations
\mforall{}L:\mBbbQ{}  List
    (0  <  ||L||
    {}\mRightarrow{}  (\mforall{}x:\mBbbQ{}
                ((qmax-list(L)  \mleq{}  x  \mLeftarrow{}{}\mRightarrow{}  (\mforall{}y\mmember{}L.y  \mleq{}  x))
                \mwedge{}  (x  \mleq{}  qmax-list(L)  \mLeftarrow{}{}\mRightarrow{}  (\mexists{}y\mmember{}L.  x  \mleq{}  y))
                \mwedge{}  (qmax-list(L)  <  x  \mLeftarrow{}{}\mRightarrow{}  (\mforall{}y\mmember{}L.y  <  x))
                \mwedge{}  (x  <  qmax-list(L)  \mLeftarrow{}{}\mRightarrow{}  (\mexists{}y\mmember{}L.  x  <  y)))))


By

---

Latex:
(RepeatFor  3  ((D  0  THENA  Auto))  THEN  SplitAndConcl)

---

Home Index