Theorems · Theorem · functional analysis

StrongDual.mem_polar_iff

∀ (𝕜 : Type u_4) [inst : NontriviallyNormedField 𝕜] {E : Type u_5} [inst_1 : AddCommMonoid E]
  [inst_2 : TopologicalSpace E] [inst_3 : Module 𝕜 E] {x' : StrongDual 𝕜 E} (s : Set E),
  x' ∈ StrongDual.polar 𝕜 s ↔ ∀ z ∈ s, ‖x' z‖ ≤ 1

Defined in

Mathlib.Analysis.LocallyConvex.Polar

Cited by

1 results in Mathlib

Foundations

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

Assumes

NontriviallyNormedFieldAddCommMonoidTopologicalSpaceModule