English
The intersection (across a finite family) of polars of finite subsets of a closed ball equals the closed ball itself.
Русский
Пересечение поляр конечного семейства подмножеств замкнутого шара эквивалентно самому замкнутому шару.
LaTeX
$$$\\bigcap_{F \\text{ finite}, F \\subseteq \\overline{B}(0,r) } \\operatorname{polar}(F) = \\overline{B}(0,r)$$$
Lean4
/-- Given a neighborhood `s` of the origin in a normed space `E`, the dual norms of all elements of
the polar `polar 𝕜 s` are bounded by a constant. -/
theorem isBounded_polar_of_mem_nhds_zero {s : Set E} (s_nhds : s ∈ 𝓝 (0 : E)) : IsBounded (StrongDual.polar 𝕜 s) :=
by
obtain ⟨a, ha⟩ : ∃ a : 𝕜, 1 < ‖a‖ := NormedField.exists_one_lt_norm 𝕜
obtain ⟨r, r_pos, r_ball⟩ : ∃ r : ℝ, 0 < r ∧ ball 0 r ⊆ s := Metric.mem_nhds_iff.1 s_nhds
exact
isBounded_closedBall.subset
(((topDualPairing 𝕜 E).flip.polar_antitone r_ball).trans <| polar_ball_subset_closedBall_div ha r_pos)
