neg_eq

Mathlib.Analysis.LocallyConvex.Basic

URI: https://scilib.ai/kg/mathlib#Balanced.neg_eq

English

If s is balanced, then its negation respects membership symmetry: -x ∈ s ⇔ x ∈ s for all x.

Русский

Если множество сбалансировано, то для каждого x верно: -x ∈ s ⇔ x ∈ s.

LaTeX

$$$\forall x, (-x)\in s \iff x\in s$ (under appropriate norm conditions)$$

Lean4

theorem neg_eq [NormOneClass 𝕜] (h : Balanced 𝕜 s) : -s = s :=
  Set.ext fun _ ↦ h.neg_mem_iff

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru