norm_coe_le_norm

Mathlib.Topology.ContinuousMap.Compact

URI: https://scilib.ai/kg/mathlib#ContinuousMap.norm_coe_le_norm

English

For a fixed f ∈ C(α,E) and x ∈ α, the value ‖f(x)‖ is bounded by the norm of f: ‖f(x)‖ ≤ ‖f‖.

Русский

Для данного f ∈ C(α,E) и x ∈ α значение ‖f(x)‖ ограничено нормой f: ‖f(x)‖ ≤ ‖f‖.

LaTeX

$$$\|f(x)\| \le \|f\| \quad (\forall x \in \alpha)$$$

Lean4

theorem norm_coe_le_norm (x : α) : ‖f x‖ ≤ ‖f‖ :=
  (mkOfCompact f).norm_coe_le_norm x

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru