# Documentation

Mathlib.Analysis.NormedSpace.HahnBanach.SeparatingDual

# Spaces with separating dual #

We introduce a typeclass SeparatingDual R V, registering that the points of the topological module V over R can be separated by continuous linear forms.

This property is satisfied for normed spaces over ℝ or ℂ (by the analytic Hahn-Banach theorem) and for locally convex topological spaces over ℝ (by the geometric Hahn-Banach theorem).

Under the assumption SeparatingDual R V, we show in SeparatingDual.exists_continuousLinearMap_apply_eq that the group of continuous linear equivalences acts transitively on the set of nonzero vectors.

class SeparatingDual (R : Type u_1) (V : Type u_2) [Ring R] [] [] [] [Module R V] :
• exists_ne_zero' : ∀ (x : V), x 0f, f x 0

Any nonzero vector can be mapped by a continuous linear map to a nonzero scalar.

When E is a topological module over a topological ring R, the class SeparatingDual R E registers that continuous linear forms on E separate points of E.

Instances
theorem SeparatingDual.exists_ne_zero {R : Type u_1} {V : Type u_2} [Ring R] [] [] [] [Module R V] [] {x : V} (hx : x 0) :
f, f x 0
theorem SeparatingDual.exists_separating_of_ne {R : Type u_1} {V : Type u_2} [Ring R] [] [] [] [Module R V] [] {x : V} {y : V} (h : x y) :
f, f x f y
theorem SeparatingDual.t1Space {R : Type u_1} {V : Type u_2} [Ring R] [] [] [] [Module R V] [] [] :
theorem SeparatingDual.t2Space {R : Type u_1} {V : Type u_2} [Ring R] [] [] [] [Module R V] [] [] :
theorem SeparatingDual.exists_eq_one {R : Type u_1} {V : Type u_2} [] [] [] [] [] [Module R V] [] {x : V} (hx : x 0) :
f, f x = 1
theorem SeparatingDual.exists_eq_one_ne_zero_of_ne_zero_pair {R : Type u_1} {V : Type u_2} [] [] [] [] [] [Module R V] [] {x : V} {y : V} (hx : x 0) (hy : y 0) :
f, f x = 1 f y 0
theorem SeparatingDual.exists_continuousLinearEquiv_apply_eq {R : Type u_1} {V : Type u_2} [] [] [] [] [] [Module R V] [] [] {x : V} {y : V} (hx : x 0) (hy : y 0) :
A, A x = y

In a topological vector space with separating dual, the group of continuous linear equivalences acts transitively on the set of nonzero vectors: given two nonzero vectors x and y, there exists A : V ≃L[R] V mapping x to y.