norm_le_norm_of_abs_le_abs

Mathlib.Analysis.Normed.Order.Lattice

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

English

If |a| ≤ |b| in a normed lattice-ordered group with a solid norm, then ∥a∥ ≤ ∥b∥.

Русский

Если |a| ≤ |b| в нормированной упорядоченной по lattices группе с прочной нормой, то ∥a∥ ≤ ∥b∥.

LaTeX

$$$|a| \le |b| \ \Rightarrow\ \|a\| \le \|b\|$$$

Lean4

theorem norm_le_norm_of_abs_le_abs {a b : α} (h : |a| ≤ |b|) : ‖a‖ ≤ ‖b‖ :=
  HasSolidNorm.solid h

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

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

Разделы

Аффилиация

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