polar_nonempty

Mathlib.Analysis.LocallyConvex.Polar

URI: https://scilib.ai/kg/mathlib#LinearMap.polar_nonempty

English

For every s, the polar B.polar(s) is nonempty.

Русский

Для любого s поляр B.polar(s) непусто.

LaTeX

$$(B.polar(s)).Nonempty$$

Lean4

theorem polar_nonempty (s : Set E) : Set.Nonempty (B.polar s) :=
  by
  use 0
  exact zero_mem_polar B s

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

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

Разделы

Аффилиация

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