mem_polar_singleton

Mathlib.Analysis.LocallyConvex.Polar

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

English

The polar of a singleton {a} is the set of y with ‖B a y‖ ≤ 1.

Русский

Полярность одиночного множества {a} состоит из всех y с условием ‖B a y‖ ≤ 1.

LaTeX

$$$B.polar(\{a\}) = \{ y \in F \mid \|B(a,y)\| \le 1 \}$$$

Lean4

theorem mem_polar_singleton {x : E} (y : F) : y ∈ B.polar { x } ↔ ‖B x y‖ ≤ 1 := by
  simp only [polar_singleton, Set.mem_setOf_eq]

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

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

Разделы

Аффилиация

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