exists_bound_of_continuous — Mathlib

English

If f has compact mul support and f is continuous, then there exists C with ∥f(x)∥ ≤ C for all x.

Русский

Если f имеет компактную множительную поддержку и непрерывна, то существует C с ∥f(x)∥ ≤ C для всех x.

LaTeX

$$∃ C, ∀ x, ‖f x‖ ≤ C$$

Lean4

@[to_additive]
theorem exists_bound_of_continuous [TopologicalSpace α] {f : α → E} (hf : HasCompactMulSupport f) (h'f : Continuous f) :
    ∃ C, ∀ x, ‖f x‖ ≤ C := by simpa using (hf.isCompact_range h'f).isBounded.exists_norm_le'

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