one_le_inv_iff_le_one

Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Order

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

English

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

Русский

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

LaTeX

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

Lean4

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

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

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

Разделы

Аффилиация

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