closedBall_inv_subset_polar_closedBall

English

Every radius 1/r element belongs to the polar of the closed ball of radius r.

Русский

Любой элемент с нормой ≤ 1/r принадлежит полярной замыканию замкнутого шара радиуса r.

LaTeX

$$$ closedBall(0, r)^{-1} \\subseteq Polar( closedBall(0, r) )$ and more precisely $\\|x'\\| ≤ 1/r \\Rightarrow x' \\in Polar( closedBall(0, r) )$$$

Lean4

theorem closedBall_inv_subset_polar_closedBall {r : ℝ} :
    closedBall (0 : StrongDual 𝕜 E) r⁻¹ ⊆ StrongDual.polar 𝕜 (closedBall (0 : E) r) := fun x' hx' x hx =>
  calc
    ‖x' x‖ ≤ ‖x'‖ * ‖x‖ := x'.le_opNorm x
    _ ≤ r⁻¹ * r :=
      (mul_le_mul (mem_closedBall_zero_iff.1 hx') (mem_closedBall_zero_iff.1 hx) (norm_nonneg _)
        (dist_nonneg.trans hx'))
    _ = r / r := (inv_mul_eq_div _ _)
    _ ≤ 1 := div_self_le_one r

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