sInter_polar_eq_closedBall — Mathlib

English

Continuation of the finite intersection property for polars on closed balls.

Русский

Продолжение свойства пересечения поляр на замкнутых шарах.

LaTeX

$$$\\cdots$$$

Lean4

theorem sInter_polar_eq_closedBall {𝕜 E : Type*} [RCLike 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] {r : ℝ}
    (hr : 0 < r) : ⋂₀ (StrongDual.polar 𝕜 '' {F | F.Finite ∧ F ⊆ closedBall (0 : E) r⁻¹}) = closedBall 0 r :=
  by
  conv_rhs => rw [← inv_inv r]
  rw [← polar_closedBall (inv_pos_of_pos hr), StrongDual.polar,
    (topDualPairing 𝕜 E).flip.sInter_polar_finite_subset_eq_polar (closedBall (0 : E) r⁻¹)]

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