---

Step * of Lemma rnexp_functionality_wrt_rleq

∀x,y:ℝ.  ((r0 ≤ x) ⇒ (x ≤ y) ⇒ (∀n:ℕ. (x^n ≤ y^n)))
BY
{ (InstLemma `rnexp-rleq` [] THEN Trivial) }

---

Latex:

---

Latex:
\mforall{}x,y:\mBbbR{}.    ((r0  \mleq{}  x)  {}\mRightarrow{}  (x  \mleq{}  y)  {}\mRightarrow{}  (\mforall{}n:\mBbbN{}.  (x\^{}n  \mleq{}  y\^{}n)))


By

---

Latex:
(InstLemma  `rnexp-rleq`  []  THEN  Trivial)

---

Home Index