inv_le_one_iff_one_le

Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Order

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

English

For a unit a with a ≥ 0, a⁻¹ ≤ 1 if and only if 1 ≤ a.

Русский

Для единицы a с a≥0: a⁻¹ ≤ 1 тогда и только тогда, когда 1 ≤ a.

LaTeX

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

Lean4

theorem inv_le_one_iff_one_le {a : Aˣ} (ha : 0 ≤ (a : A)) : (↑a⁻¹ : A) ≤ 1 ↔ 1 ≤ a := by
  simpa using CStarAlgebra.inv_le_iff ha (b := 1) (by simp)

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

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

Разделы

Аффилиация

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