dual_empty

Mathlib.Analysis.Convex.Cone.Dual

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

English

The dual cone of an empty set is the whole ambient space (top cone).

Русский

Дуал пустого множества равен всему пространству.

LaTeX

$$dual p ∅ = ⊤$$

Lean4

@[simp]
theorem dual_empty : dual p ∅ = ⊤ := by ext; simp

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

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

Разделы

Аффилиация

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