---

Step * of Lemma qmax_ub

∀a,b,c:ℚ.  (a ≤ qmax(b;c) ⇐⇒ (a ≤ b) ∨ (a ≤ c))
BY
{ xxx((UnivCD THENA Auto) THEN Unfold `qmax` 0 THEN SplitOnConclITE THEN Auto)xxx }

1
1. a : ℚ
2. b : ℚ
3. c : ℚ
4. ¬(b ≤ c)
5. a ≤ c
⊢ a ≤ b

---

Latex:

---

Latex:
\mforall{}a,b,c:\mBbbQ{}.    (a  \mleq{}  qmax(b;c)  \mLeftarrow{}{}\mRightarrow{}  (a  \mleq{}  b)  \mvee{}  (a  \mleq{}  c))


By

---

Latex:
xxx((UnivCD  THENA  Auto)  THEN  Unfold  `qmax`  0  THEN  SplitOnConclITE  THEN  Auto)xxx

---

Home Index