Theorems · Theorem · functional analysis

WeakDual.exists_countable_separating

∀ (𝕜 : Type u_1) (E : Type u_3) [inst : NontriviallyNormedField 𝕜] [inst_1 : SeminormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] [TopologicalSpace.SeparableSpace E],
  ∃ gs, (∀ (n : ℕ), Continuous (gs n)) ∧ ∀ ⦃x y : WeakDual 𝕜 E⦄, x ≠ y → ∃ n, gs n x ≠ gs n y

In a separable normed space, there exists a sequence of continuous functions that separates points of the weak dual.

Defined in

Mathlib.Analysis.Normed.Module.WeakDual

Cited by

1 results in Mathlib

Foundations

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

Assumes

NontriviallyNormedFieldSeminormedAddCommGroupNormedSpaceTopologicalSpace.SeparableSpace