convexBodySum_neg_mem

Mathlib.NumberTheory.NumberField.CanonicalEmbedding.ConvexBody

URI: https://scilib.ai/kg/mathlib#NumberField.mixedEmbedding.convexBodySum_neg_mem

← MathLib Explorer

English

If x belongs to convexBodySum K B, then -x also belongs to convexBodySum K B.

Русский

Если x ∈ convexBodySum K B, то и -x ∈ convexBodySum K B.

LaTeX

$$x ∈ convexBodySum K B \\Rightarrow -x ∈ convexBodySum K B$$

Lean4

theorem convexBodySum_neg_mem {x : mixedSpace K} (hx : x ∈ (convexBodySum K B)) : -x ∈ (convexBodySum K B) :=
  by
  rw [Set.mem_setOf, convexBodySumFun_neg]
  exact hx

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

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

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

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