enorm_eq_iSup_enorm

Mathlib.Topology.ContinuousMap.Compact

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

English

The norm equals the pointwise supremum: ‖f‖ = ⨆ x∈α, ‖f(x)‖.

Русский

Норма равна верхней границе по точкам: ‖f‖ = ⨆_{x∈α} ‖f(x)‖.

LaTeX

$$$\|f\| = \sup_{x \in \alpha} \|f(x)\|$$$

Lean4

theorem enorm_eq_iSup_enorm : ‖f‖ₑ = ⨆ x, ‖f x‖ₑ :=
  (mkOfCompact f).enorm_eq_iSup_enorm

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

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

Разделы

Аффилиация

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