---

Step * of Lemma rmin-rmax-real-decomp

∀[r:ℝ]. ((rmin(|r|;rmax(r0;r)) + rmax(-(|r|);rmin(r0;r))) = r)
BY
{ Auto }

1
1. r : ℝ
⊢ (rmin(|r|;rmax(r0;r)) + rmax(-(|r|);rmin(r0;r))) = r

---

Latex:

---

Latex:
\mforall{}[r:\mBbbR{}].  ((rmin(|r|;rmax(r0;r))  +  rmax(-(|r|);rmin(r0;r)))  =  r)


By

---

Latex:
Auto

---

Home Index