posPart_neg — Mathlib

English

There exists a NegPart operation on A defined by negPart := cfcₙ (·⁻ : ℝ → ℝ).

Русский

Существует операция NegPart на A, определяемая как negPart = cfcₙ (t⁻).

LaTeX

$$$a^- = \mathrm{cfc}_{\mathbb{R}}(t \mapsto t^-)(a)$$$

Lean4

@[simp]
theorem posPart_neg (a : A) : (-a)⁺ = a⁻ := by
  by_cases ha : IsSelfAdjoint a
  · rw [posPart_def, negPart_def, ← cfcₙ_comp_neg _ _]
    congr! 2
  · have ha' : ¬IsSelfAdjoint (-a) := fun h ↦ ha (by simpa using h.neg)
    rw [posPart_def, negPart_def, cfcₙ_apply_of_not_predicate a ha, cfcₙ_apply_of_not_predicate _ ha']

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