isBoundedUnder_le_exp_comp — Mathlib

English

For any function f, the property that exp(f) is bounded above along l is equivalent to f being bounded above along l, because exp is strictly increasing and unbounded.

Русский

Для любой функции f свойство того, что exp(f) ограничено сверху вдоль l, эквивалентно тому, что f ограничено сверху вдоль l, поскольку exp возрастает и неограничен.

LaTeX

$$$\\text{IsBoundedUnder}(\\le, l, \\exp \\circ f) \\quad\\leftrightarrow\\quad \\text{IsBoundedUnder}(\\le, l, f).$$$

Lean4

@[simp]
theorem isBoundedUnder_le_exp_comp {f : α → ℝ} :
    (IsBoundedUnder (· ≤ ·) l fun x => exp (f x)) ↔ IsBoundedUnder (· ≤ ·) l f :=
  exp_monotone.isBoundedUnder_le_comp_iff tendsto_exp_atTop

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