isBoundedUnder_abs — Mathlib

English

For a concave on C, the boundedness of |f| near x0 implies boundedness of f near x0 when C contains x0 in its neighborhood.

Русский

Для выпуклой на C, ограниченность |f| в окрестности x0 эквивалентна ограниченности f в окрестности x0 при определенной постановке.

LaTeX

$$$ (\\mathcal{N}_{x_0}).IsBoundedUnder (≤) |f| \\iff (\\mathcal{N}_{x_0}).IsBoundedUnder (≤) f $$$

Lean4

theorem isBoundedUnder_abs (hf : ConcaveOn ℝ C f) {x₀ : E} (hC : C ∈ 𝓝 x₀) :
    (𝓝 x₀).IsBoundedUnder (· ≤ ·) |f| ↔ (𝓝 x₀).IsBoundedUnder (· ≥ ·) f := by
  simpa [Pi.neg_def, Pi.abs_def] using hf.neg.isBoundedUnder_abs hC

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