polar_singleton — Mathlib

English

The intersection of polars over a finite set of elements from a polar construction equals the polar of that finite subset.

Русский

Пересечение поляр над конечной коллекцией элементов равно полю поляр для этого конечного подмножества.

LaTeX

$$$\bigcap_{a \in s} B.polar(\{a\}) = B.polar(s)$$$

Lean4

@[simp]
theorem polar_singleton {a : E} : B.polar { a } = {y | ‖B a y‖ ≤ 1} :=
  le_antisymm (fun _ hy => hy _ rfl)
    (fun y hy => (polar_mem_iff _ _ _).mp (fun _ hb => by rw [Set.mem_singleton_iff.mp hb]; exact hy))

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