---

Step * 1 of Lemma rpositive-rmax


1. x : ℝ@i
2. y : ℝ@i
3. rpositive(rmax(x;y))@i
⊢ rpositive(x) ∨ rpositive(y)
BY
{ (D (-1)
   THEN RepUR ``rmax`` (-1)⋅
   THEN (RWO "imax_strict_ub" (-1) THENA Auto)
   THEN ParallelLast
   THEN With ⌜n⌝ (D 0)⋅
   THEN Auto) }

---

Latex:

---

Latex:

1.  x  :  \mBbbR{}@i
2.  y  :  \mBbbR{}@i
3.  rpositive(rmax(x;y))@i
\mvdash{}  rpositive(x)  \mvee{}  rpositive(y)


By

---

Latex:
(D  (-1)
  THEN  RepUR  ``rmax``  (-1)\mcdot{}
  THEN  (RWO  "imax\_strict\_ub"  (-1)  THENA  Auto)
  THEN  ParallelLast
  THEN  With  \mkleeneopen{}n\mkleeneclose{}  (D  0)\mcdot{}
  THEN  Auto)

---

Home Index