negPart_eq_neg — Mathlib

English

Let a be as above. The negative part a⁻ equals -a if and only if a ≤ 0.

Русский

Пусть a — как выше. Отрицательная часть a⁻ равна -a тогда и только тогда, когда a ≤ 0.

LaTeX

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

Lean4

theorem negPart_eq_neg (a : A) : a⁻ = -a ↔ a ≤ 0 :=
  by
  rw [← neg_inj, neg_neg, eq_comm]
  refine ⟨fun ha ↦ by rw [ha, neg_nonpos]; exact negPart_nonneg a, fun ha ↦ ?_⟩
  rw [← neg_nonneg] at ha
  rw [negPart_def, ← cfcₙ_neg]
  have _ : IsSelfAdjoint a := neg_neg a ▸ (IsSelfAdjoint.neg <| .of_nonneg ha)
  conv_lhs => rw [← cfcₙ_id ℝ a]
  refine cfcₙ_congr fun x hx ↦ ?_
  rw [Unitization.quasispectrum_eq_spectrum_inr ℝ, ← neg_neg x, ← Set.mem_neg, spectrum.neg_eq, ← Unitization.inr_neg, ←
    Unitization.quasispectrum_eq_spectrum_inr ℝ] at hx
  rw [← neg_eq_iff_eq_neg, eq_comm]
  simpa using quasispectrum_nonneg_of_nonneg _ ha _ hx

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