neg_coe — Mathlib

English

For any submodule p of M, negating its underlying set yields the same set; equivalently, the underlying set is closed under taking additive inverses.

Русский

Для подмодуля p модуля M множество, полученное взятие противоположного по знаку, совпадает с исходным множеством; то есть множество замкнуто относительно операции взятия противоположного.

LaTeX

$$$-(p \\;\\text{as a set}) = p$$$

Lean4

theorem neg_coe : -(p : Set M) = p :=
  Set.ext fun _ => p.neg_mem_iff

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