balanced_neg

Mathlib.Analysis.LocallyConvex.Basic

URI: https://scilib.ai/kg/mathlib#balanced_neg

English

For a balanced set s, the negation set -s equals s (under NormOneField assumptions).

Русский

Для сбалансированного множества s выполняется -s = s (при предпосылке NormOneClass).

LaTeX

$$$\text{Balanced}_{\mathfrak{k}}(s) \Rightarrow -s = s$$$

Lean4

@[simp]
theorem balanced_neg : Balanced 𝕜 (-s) ↔ Balanced 𝕜 s :=
  ⟨fun h ↦ neg_neg s ▸ h.neg, fun h ↦ h.neg⟩

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

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

Разделы

Аффилиация

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