norm_const_eq

Mathlib.Topology.ContinuousMap.Bounded.Normed

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

← MathLib Explorer

English

If α is nonempty, then the norm of const α b equals ‖b‖.

Русский

Если α не пусто, то норма константной функции const α b равна ‖b‖.

LaTeX

$$$‖const\\,\\alpha b‖ = ‖b‖$$$

Lean4

@[simp]
theorem norm_const_eq [h : Nonempty α] (b : β) : ‖const α b‖ = ‖b‖ :=
  le_antisymm (norm_const_le b) <| h.elim fun x => (const α b).norm_coe_le_norm x

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

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

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

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