polar_empty

Mathlib.Analysis.LocallyConvex.Polar

URI: https://scilib.ai/kg/mathlib#StrongDual.polar_empty

English

The polar of the empty set is the entire dual space: polar 𝕜 ∅ = StrongDual 𝕜 M.

Русский

Поляр пустого множества равна всему двойственному пространству: polar 𝕜 ∅ = StrongDual 𝕜 M.

LaTeX

$$$\operatorname{polar}_{\mathbb{K}}(\emptyset) = \mathrm{StrongDual}_{\mathbb{K}}(M)$$$

Lean4

@[simp]
theorem polar_empty : polar 𝕜 (∅ : Set E) = Set.univ :=
  LinearMap.polar_empty _

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

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

Разделы

Аффилиация

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