posPart_mul_negPart — Mathlib

English

The positive and negative parts are orthogonal in the sense that a⁺ a⁻ = 0.

Русский

Положительная и отрицательная части взаимно ортогональны: a⁺ a⁻ = 0.

LaTeX

$$$a^+ \cdot a^- = 0$$$

Lean4

@[simp]
theorem posPart_mul_negPart (a : A) : a⁺ * a⁻ = 0 :=
  by
  rw [posPart_def, negPart_def]
  by_cases ha : IsSelfAdjoint a
  · rw [← cfcₙ_mul _ _, ← cfcₙ_zero ℝ a]
    refine cfcₙ_congr (fun x _ ↦ ?_)
    simp only [_root_.posPart_def, _root_.negPart_def]
    simpa using le_total x 0
  · simp [cfcₙ_apply_of_not_predicate a ha]

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