polar_mem

Mathlib.Analysis.LocallyConvex.Polar

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

English

For each s, the polar B.polar(s) is closed in the weak topology on F induced by B.flip.

Русский

Для каждого множества s поляр B.polar(s) является замкнутым в слабой топологии на F, индуцируемой B.flip.

LaTeX

$$IsClosed_{Weak(B.flip)}(B.polar(s))$$

Lean4

theorem polar_mem (s : Set E) (y : F) (hy : y ∈ B.polar s) : ∀ x ∈ s, ‖B x y‖ ≤ 1 :=
  hy

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

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

Разделы

Аффилиация

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