norm_abs_eq_norm

Mathlib.Analysis.Normed.Order.Lattice

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

English

For any a in a normed lattice-ordered group with a solid norm, ∥|a|∥ = ∥a∥.

Русский

Для любого a в нормированной упорядоченной группе с солидной нормой выполняется ∥|a|∥ = ∥a∥.

LaTeX

$$$\|\,|a|\,\| = \|a\|$$$

Lean4

theorem norm_abs_eq_norm (a : α) : ‖|a|‖ = ‖a‖ :=
  (solid (abs_abs a).le).antisymm (solid (abs_abs a).symm.le)

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

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

Разделы

Аффилиация

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