polar_AbsConvex — Mathlib

English

The polar of any set is AbsConvex in the ambient space.

Русский

Поляр множества является AbsConvex во внешнем пространстве.

LaTeX

$$$\\operatorname{polar}(s)\\ \\text{is AbsConvex in } 𝕜$$$

Lean4

theorem polar_AbsConvex : AbsConvex 𝕜 (B.polar s) :=
  by
  rw [polar_eq_biInter_preimage]
  exact
    AbsConvex.iInter₂ fun i hi =>
      ⟨balanced_closedBall_zero.mulActionHom_preimage (f := (B i : (F →ₑ[(RingHom.id 𝕜)] 𝕜))),
        (convex_closedBall _ _).linear_preimage (B i)⟩

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