English
If e > 1, the map m ↦ toNNReal(ne_zero_of_lt he) m is strictly monotone.
Русский
Пусть e > 1. Тогда отображение m ↦ toNNReal(ne_zero_of_lt he) m строго монотонно по отношению к m.
LaTeX
$$If 1 < e, then the function m ↦ toNNReal(ne_zero_of_lt e) (m) is strictly monotone.$$
Lean4
/-- The map `toNNReal` is strictly monotone whenever `1 < e`. -/
theorem toNNReal_strictMono {e : ℝ≥0} (he : 1 < e) : StrictMono (toNNReal (ne_zero_of_lt he)) :=
by
intro x y hxy
simp only [toNNReal, MonoidWithZeroHom.coe_mk, ZeroHom.coe_mk]
split_ifs with hx hy hy
· simp only [hy, not_lt_zero'] at hxy
· exact zpow_pos he.bot_lt _
· simp only [hy, not_lt_zero'] at hxy
· rw [zpow_lt_zpow_iff_right₀ he, Multiplicative.toAdd_lt, ← coe_lt_coe, coe_unzero hx, WithZero.coe_unzero hy]
exact hxy
