---

Step * 1 1 1 of Lemma rlog-rexp

.....antecedent..... 
1. x : ℝ
⊢ maps-compact((-∞, ∞);(r0, ∞);x.e^x)
BY
{ (BLemma `monotone-maps-compact` THEN Auto) }

1
1. x : ℝ
2. x1 : {t:ℝ| t ∈ (-∞, ∞)} @i
⊢ e^x1 ∈ (r0, ∞)

---

Latex:

---

Latex:
.....antecedent..... 
1.  x  :  \mBbbR{}
\mvdash{}  maps-compact((-\minfty{},  \minfty{});(r0,  \minfty{});x.e\^{}x)


By

---

Latex:
(BLemma  `monotone-maps-compact`  THEN  Auto)

---

Home Index