norm_ofDual

Mathlib.Analysis.Normed.Group.Constructions

URI: https://scilib.ai/kg/mathlib#norm_ofDual

English

The norm on the dual object Eᵒᵈ is compatible with the norm on E, via the embedding of the dual, i.e., ‖ofDual x‖ = ‖x‖.

Русский

Норма на двойственной структуре совместима с нормой на E: ‖ofDual x‖ = ‖x‖.

LaTeX

$$$‖ofDual\,x‖ = ‖x‖$$$

Lean4

@[simp]
theorem norm_ofDual (x : Eᵒᵈ) : ‖ofDual x‖ = ‖x‖ :=
  rfl

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

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

Разделы

Аффилиация

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