neg_mem_iff — Mathlib

English

If s is balanced (NormOneClass assumed), then for any x, -x ∈ s iff x ∈ s.

Русский

Если s сбалансировано, то для любого x выполняется, что -x ∈ s тогда и только тогда, когда x ∈ s.

LaTeX

$$$[\text{NormOneClass }]\text{ Balanced }(s) \Rightarrow \forall x, -x \in s \iff x \in s$$$

Lean4

theorem neg_mem_iff [NormOneClass 𝕜] (h : Balanced 𝕜 s) {x : E} : -x ∈ s ↔ x ∈ s :=
  ⟨fun hx ↦ by simpa using h.smul_mem (a := -1) (by simp) hx, fun hx ↦ by simpa using h.smul_mem (a := -1) (by simp) hx⟩

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