exp_strictMono — Mathlib

English

The exponential map on EReal is strictly increasing.

Русский

Переобразование экспоненты на EReal строго возрастает.

LaTeX

$$$\text{StrictMono}(\exp): \text{StrictMono}(\exp)$$$

Lean4

theorem exp_strictMono : StrictMono exp := by
  intro x y h
  induction x
  · rw [exp_bot, pos_iff_ne_zero, ne_eq, exp_eq_zero_iff]
    exact h.ne'
  · induction y
    · simp at h
    · simp_rw [exp_coe]
      exact ENNReal.ofReal_lt_ofReal_iff'.mpr ⟨Real.exp_lt_exp_of_lt (mod_cast h), Real.exp_pos _⟩
    · simp
  · exact (not_top_lt h).elim

Похожие утверждения