---

Step * of Lemma rat2real-qmin

∀[a,b:ℚ].  (rat2real(qmin(a;b)) = rmin(rat2real(a);rat2real(b)))
BY
{ (Auto
   THEN Assert ⌜(rat2real(qmin(a;b)) ≤ rmin(rat2real(a);rat2real(b)))
                ∧ (rmin(rat2real(a);rat2real(b)) ≤ rat2real(qmin(a;b)))⌝⋅
   THEN Auto
   THEN ((BLemma `rmin_lb` ORELSE BLemma `rmin_ub`) THENA Auto)
   THEN (RWO "rleq-rat2real" 0 THENA Auto)
   THEN RWO "qmin_ub qmin_lb" 0
   THEN Auto) }

1
1. a : ℚ
2. b : ℚ
3. rat2real(qmin(a;b)) ≤ rmin(rat2real(a);rat2real(b))
⊢ ((a ≤ a) ∧ (a ≤ b)) ∨ ((b ≤ a) ∧ (b ≤ b))

---

Latex:

---

Latex:
\mforall{}[a,b:\mBbbQ{}].    (rat2real(qmin(a;b))  =  rmin(rat2real(a);rat2real(b)))


By

---

Latex:
(Auto
  THEN  Assert  \mkleeneopen{}(rat2real(qmin(a;b))  \mleq{}  rmin(rat2real(a);rat2real(b)))
                            \mwedge{}  (rmin(rat2real(a);rat2real(b))  \mleq{}  rat2real(qmin(a;b)))\mkleeneclose{}\mcdot{}
  THEN  Auto
  THEN  ((BLemma  `rmin\_lb`  ORELSE  BLemma  `rmin\_ub`)  THENA  Auto)
  THEN  (RWO  "rleq-rat2real"  0  THENA  Auto)
  THEN  RWO  "qmin\_ub  qmin\_lb"  0
  THEN  Auto)

---

Home Index