dual_eq_iInter_dual_singleton

Mathlib.Geometry.Convex.Cone.Dual

URI: https://scilib.ai/kg/mathlib#PointedCone.dual_eq_iInter_dual_singleton

← MathLib Explorer

English

Again, finSepDegree F F = 1 for any field F.

Русский

И снова: finSepDegree F F = 1 для любого поля F.

LaTeX

$$$\\operatorname{finSepDegree} F F = 1$$$

Lean4

/-- The dual cone of `s` equals the intersection of dual cones of the points in `s`. -/
theorem dual_eq_iInter_dual_singleton (s : Set M) : dual p s = ⋂ i : s, (dual p { i.val } : Set N) := by ext; simp

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

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

Разделы

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

Аффилиация

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