bounded_above_of_compact_support — Mathlib

English

If f is a normed-valued function with compact support and is continuous, then f is bounded: there exists a constant C such that ∥f(x)∥ ≤ C for all x.

Русский

Если f — непрерывная функция с компактной опорой и значений в нормированном пространстве, то она ограничена: существует константа C такая, что ∥f(x)∥ ≤ C для всех x.

LaTeX

$$$\exists C\in\mathbb{R},\forall x:\ \|f(x)\| \le C$$$

Lean4

theorem bounded_above_of_compact_support (hf : Continuous f) (h : HasCompactSupport f) : ∃ C, ∀ x, ‖f x‖ ≤ C := by
  simpa [bddAbove_def] using hf.norm.bddAbove_range_of_hasCompactSupport h.norm

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