norm_normComp

Mathlib.Topology.ContinuousMap.Bounded.Normed

URI: https://scilib.ai/kg/mathlib#BoundedContinuousFunction.norm_normComp

English

The norm of the norm-processed function is equal to the norm of the original function: ∥f.normComp∥ = ∥f∥.

Русский

Норма обработанной функцией по норме сохраняется: ∥f.normComp∥ = ∥f∥.

LaTeX

$$$\|f.normComp\| = \|f\|$$$

Lean4

@[simp]
theorem norm_normComp : ‖f.normComp‖ = ‖f‖ := by simp only [norm_eq, coe_normComp, norm_norm, Function.comp]

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

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

Разделы

Аффилиация

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