neg_mem_range_root_iff — Mathlib

English

The negation preserves membership in the range of the root map: -x ∈ range P.root iff x ∈ range P.root.

Русский

Отрицание сохраняет принадлежность диапазона корня: -x ∈ range P.root ⇔ x ∈ range P.root.

LaTeX

$$$ -x \in \mathrm{range}(P.root) \;\Leftrightarrow\; x \in \mathrm{range}(P.root) $$$

Lean4

theorem neg_mem_range_root_iff {x : M} : -x ∈ range P.root ↔ x ∈ range P.root :=
  by
  suffices ∀ x : M, -x ∈ range P.root → x ∈ range P.root
    by
    refine ⟨this x, fun h ↦ ?_⟩
    rw [← neg_neg x] at h
    exact this (-x) h
  intro y ⟨i, hi⟩
  exact ⟨P.reflectionPerm i i, by simp [neg_eq_iff_eq_neg.mpr hi]⟩

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