norm_inr

Mathlib.Analysis.Normed.Algebra.Unitization

URI: https://scilib.ai/kg/mathlib#Unitization.norm_inr

English

For a in A, the unitization inr a has the same norm as a: ||(a)|| = ||a||.

Русский

Для a из A норма элементa inr a совпадает с нормой a: ||(a)|| = ||a||.

LaTeX

$$$$\\|\\,(a: Unitization 𝕜 A)\\| = \\|a\\|.$$$$

Lean4

theorem norm_inr (a : A) : ‖(a : Unitization 𝕜 A)‖ = ‖a‖ := by simp [norm_eq_sup]

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

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

Разделы

Аффилиация

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