---

Step * of Lemma qmin-eq-iff-1

∀[q,r:ℚ].  uiff(qmin(q;r) = q ∈ ℚ;q ≤ r)
BY
{ ((UnivCD THENA Auto) THEN (RWO "qmin-eq-iff" 0 THENA Auto) THEN Auto) }

1
1. q : ℚ
2. r : ℚ
3. (r ≤ q) ⇒ (q = r ∈ ℚ)
4. (q ≤ r) ⇒ (q = q ∈ ℚ)
⊢ q ≤ r

---

Latex:

---

Latex:
\mforall{}[q,r:\mBbbQ{}].    uiff(qmin(q;r)  =  q;q  \mleq{}  r)


By

---

Latex:
((UnivCD  THENA  Auto)  THEN  (RWO  "qmin-eq-iff"  0  THENA  Auto)  THEN  Auto)

---

Home Index