neg_mem_range_coroot_iff — Mathlib

English

The negation preserves membership in the range of the coroot map: -x ∈ range P.coroot ↔ x ∈ range P.coroot.

Русский

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

LaTeX

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

Lean4

theorem neg_mem_range_coroot_iff {x : N} : -x ∈ range P.coroot ↔ x ∈ range P.coroot :=
  P.flip.neg_mem_range_root_iff

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