hasCompactSupport_norm_iff — Mathlib

English

If f: α → E has compact (or bounded) range, then its norm is bounded, i.e., there exists C with ∥f(x)∥ ≤ C for all x.

Русский

Если отображение f: α → E имеет ограниченный или компактный образ, то нормa ‖f(x)‖ ограничена сверху: существует C, такое что ∥f(x)∥ ≤ C для всех x.

LaTeX

$$$\\exists C \\; \\forall x, \\|f(x)\\| ≤ C$$$

Lean4

theorem hasCompactSupport_norm_iff : (HasCompactSupport fun x => ‖f x‖) ↔ HasCompactSupport f :=
  hasCompactSupport_comp_left norm_eq_zero

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