inv_le_one

Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Order

URI: https://scilib.ai/kg/mathlib#CStarAlgebra.inv_le_one

English

If a ≥ 1 as a unit, then a⁻¹ ≤ 1.

Русский

Если единица a ≥ 1, то a⁻¹ ≤ 1.

LaTeX

$${a : A^{\\times}} ha : 1 ≤ a \\Rightarrow a^{-1} ≤ 1$$

Lean4

theorem inv_le_one {a : Aˣ} (ha : 1 ≤ a) : (↑a⁻¹ : A) ≤ 1 :=
  CStarAlgebra.inv_le_one_iff_one_le (zero_le_one.trans ha) |>.mpr ha

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

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

Разделы

Аффилиация

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