Theorems · Theorem · functional analysis

SeparatingDual.eq_iff_forall_dual_eq

∀ {R : Type u_1} {V : Type u_2} [inst : Ring R] [inst_1 : AddCommGroup V] [inst_2 : TopologicalSpace V]
  [inst_3 : TopologicalSpace R] [inst_4 : Module R V] [SeparatingDual R V] {x y : V},
  x = y ↔ ∀ (g : StrongDual R V), g x = g y

See also geometric_hahn_banach_point_point.

Defined in

Mathlib.Analysis.LocallyConvex.SeparatingDual

Cited by

5 results in Mathlib

Foundations

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

Assumes

RingAddCommGroupTopologicalSpaceTopologicalSpaceModuleSeparatingDual