posPart_eq_self — Mathlib

English

Let a be an element of an ordered star-algebra with the continuous functional calculus. The positive part a⁺ equals a if and only if a is nonnegative, i.e., a⁺ = a ⇔ 0 ≤ a.

Русский

Пусть a — элемент упорядоченного алгебраического пространства со скалярным умножением и непрерывным функциональным вычислителем. Положительная часть a⁺ равна a тогда и только тогда, когда a неотрицательно, то есть a⁺ = a ⇔ 0 ≤ a.

LaTeX

$$$a^+ = a \\iff 0 \\le a$$$

Lean4

theorem posPart_eq_self (a : A) : a⁺ = a ↔ 0 ≤ a :=
  by
  refine ⟨fun ha ↦ ha ▸ posPart_nonneg a, fun ha ↦ ?_⟩
  conv_rhs => rw [← cfcₙ_id ℝ a]
  rw [posPart_def]
  refine cfcₙ_congr (fun x hx ↦ ?_)
  simpa [_root_.posPart_def] using quasispectrum_nonneg_of_nonneg a ha x hx

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