isBoundedUnder_ge_exp_comp — Mathlib

English

For any l and any function f, the values exp(f(x)) are bounded below by 0, since exp takes only positive values.

Русский

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

LaTeX

$$$\\forall x:\\Exp(f(x)) \\ge 0$.$$

Lean4

@[simp]
theorem isBoundedUnder_ge_exp_comp (l : Filter α) (f : α → ℝ) : IsBoundedUnder (· ≥ ·) l fun x => exp (f x) :=
  isBoundedUnder_of ⟨0, fun _ => (exp_pos _).le⟩

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