inr_nonneg_iff — Mathlib

English

For every a in A, 0 ≤ a (inside A) is equivalent to 0 ≤ a viewed as an element of the unitization A⁺¹.

Русский

Для каждого элемента a из A выполняется, что 0 ≤ a в A тогда и только тогда, когда 0 ≤ a, считаясь элементом единичирования A⁺¹.

LaTeX

$$$0 \\le (a : A^{+1}) \\iff 0 \\le a$$$

Lean4

@[simp, norm_cast]
theorem inr_nonneg_iff {a : A} : 0 ≤ (a : A⁺¹) ↔ 0 ≤ a :=
  by
  by_cases ha : IsSelfAdjoint a
  · exact inr_zero ℂ (A := A) ▸ inr_le_iff 0 a
  · refine ⟨?_, ?_⟩
    all_goals refine fun h ↦ (ha ?_).elim
    · exact isSelfAdjoint_inr (R := ℂ) |>.mp <| .of_nonneg h
    · exact .of_nonneg h

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