subset_dual_dual

Mathlib.Analysis.Convex.Cone.Dual

URI: https://scilib.ai/kg/mathlib#ProperCone.subset_dual_dual

English

Any set is a subset of its double dual cone.

Русский

Любое множество является подмножеством своего двойного дуального конуса.

LaTeX

$$s ⊆ dual p.flip (dual p s)$$

Lean4

/-- Any set is a subset of its double dual cone. -/
theorem subset_dual_dual : s ⊆ dual p.flip (dual p s) := fun _x hx _y hy ↦ hy hx

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

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

Разделы

Аффилиация

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