---

Step * of Lemma qmin-list-bounds

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

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

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

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

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

---

Latex:

---

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


By

---

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

---

Home Index