Theorems · Theorem · functional analysis

NormedSpace.smul_mem_polar

∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : SeminormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {s : Set E} {x' : StrongDual 𝕜 E} {c : 𝕜},
  (∀ z ∈ s, ‖x' z‖ ≤ ‖c‖) → c⁻¹ • x' ∈ StrongDual.polar 𝕜 s

If x' is a StrongDual 𝕜 E element such that the norms ‖x' z‖ are bounded for z ∈ s, then a small scalar multiple of x' is in polar 𝕜 s.

Defined in

Mathlib.Analysis.Normed.Module.Dual

Cited by

0 results in Mathlib

Foundations

Depth 167 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

NontriviallyNormedFieldSeminormedAddCommGroupNormedSpace