negAt_symm — Mathlib

English

NegAt is its own inverse.

Русский

NegAt есть собственное обратное.

LaTeX

$$negAt_symm : (negAt s).symm = negAt s$$

Lean4

/-- `negAt` is its own inverse. -/
@[simp]
theorem negAt_symm : (negAt s).symm = negAt s := by
  ext x w
  · by_cases hw : w ∈ s
    ·
      simp_rw [negAt_apply_isReal_and_mem _ hw, negAt, prodCongr_symm, prodCongr_apply, piCongrRight_symm_apply,
        if_pos hw, symm_neg, neg_apply]
    ·
      simp_rw [negAt_apply_isReal_and_notMem _ hw, negAt, prodCongr_symm, prodCongr_apply, piCongrRight_symm_apply,
        if_neg hw, refl_symm, refl_apply]
  · rfl

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