norm_eq_iSup_norm

Mathlib.Topology.ContinuousMap.Compact

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

English

A repeated statement: ‖f.restrict K‖ ≤ ‖f.restrict L‖ whenever K ≤ L in TopologicalSpace.Compacts.

Русский

Повторение: ‖f.restrict K‖ ≤ ‖f.restrict L‖ при K ≤ L.

LaTeX

$$$\|f.restrict K\| \le \|f.restrict L\|$$$

Lean4

theorem norm_eq_iSup_norm : ‖f‖ = ⨆ x : α, ‖f x‖ :=
  (mkOfCompact f).norm_eq_iSup_norm

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

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

Разделы

Аффилиация

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