exp_strictMono — Mathlib

English

The exponential function is strictly increasing: if x < y then exp(x) < exp(y).

Русский

Функция экспоненты строго возрастающая: если x < y, то exp(x) < exp(y).

LaTeX

$$x < y \Rightarrow \exp x < \exp y$$

Lean4

@[mono]
theorem exp_strictMono : StrictMono exp := fun x y h =>
  by
  rw [← sub_add_cancel y x, Real.exp_add]
  exact (lt_mul_iff_one_lt_left (exp_pos _)).2 (lt_of_lt_of_le (by linarith) (add_one_le_exp_of_nonneg (by linarith)))

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