norm_eq_norm'

Mathlib.Analysis.Normed.Group.Continuity

URI: https://scilib.ai/kg/mathlib#Inseparable.norm_eq_norm'

English

If u and v are inseparable in E, then their nnnorms are equal: ‖u‖₊ = ‖v‖₊.

Русский

Если u и v неразделимы в E, то их nnnorm равны: ‖u‖₊ = ‖v‖₊.

LaTeX

$$$ \text{Inseparable}(u,v) \Rightarrow \|u\|_+ = \|v\|_+. $$$

Lean4

@[to_additive Inseparable.norm_eq_norm]
theorem norm_eq_norm' {u v : E} (h : Inseparable u v) : ‖u‖ = ‖v‖ :=
  h.map continuous_norm' |>.eq

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

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

Разделы

Аффилиация

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