Theorems · Theorem · functional analysis

SeparatingDual.exists_eq_one

∀ {R : Type u_1} {V : Type u_2} [inst : Field R] [inst_1 : AddCommGroup V] [inst_2 : TopologicalSpace R]
  [inst_3 : TopologicalSpace V] [IsTopologicalRing R] [inst_5 : Module R V] [SeparatingDual R V] {x : V},
  x ≠ 0 → ∃ f, f x = 1

Defined in

Mathlib.Analysis.LocallyConvex.SeparatingDual

Cited by

4 results in Mathlib

Foundations

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

Assumes

FieldAddCommGroupTopologicalSpaceTopologicalSpaceIsTopologicalRingModuleSeparatingDual