---

Step * of Lemma rmin_strict_lb

∀x,y,z:ℝ.  ((x < z) ∨ (y < z) ⇐⇒ rmin(x;y) < z)
BY
{ (Auto
   THEN SplitOrHyps
   THEN Try ((RepeatFor 2 (ParallelLast) THEN RepUR ``rmin`` 0 THEN (RWO "imin_unfold" 0 THENA Auto) THEN AutoSplit))) }

1
1. x : ℝ
2. y : ℝ
3. z : ℝ
4. rmin(x;y) < z
⊢ (x < z) ∨ (y < z)

---

Latex:

---

Latex:
\mforall{}x,y,z:\mBbbR{}.    ((x  <  z)  \mvee{}  (y  <  z)  \mLeftarrow{}{}\mRightarrow{}  rmin(x;y)  <  z)


By

---

Latex:
(Auto
  THEN  SplitOrHyps
  THEN  Try  ((RepeatFor  2  (ParallelLast)
                        THEN  RepUR  ``rmin``  0
                        THEN  (RWO  "imin\_unfold"  0  THENA  Auto)
                        THEN  AutoSplit)))

---

Home Index