# Documentation

Mathlib.Analysis.NormedSpace.HahnBanach.Separation

# Separation Hahn-Banach theorem #

In this file we prove the geometric Hahn-Banach theorem. For any two disjoint convex sets, there exists a continuous linear functional separating them, geometrically meaning that we can intercalate a plane between them.

We provide many variations to stricten the result under more assumptions on the convex sets:

• geometric_hahn_banach_open: One set is open. Weak separation.
• geometric_hahn_banach_open_point, geometric_hahn_banach_point_open: One set is open, the other is a singleton. Weak separation.
• geometric_hahn_banach_open_open: Both sets are open. Semistrict separation.
• geometric_hahn_banach_compact_closed, geometric_hahn_banach_closed_compact: One set is closed, the other one is compact. Strict separation.
• geometric_hahn_banach_point_closed, geometric_hahn_banach_closed_point: One set is closed, the other one is a singleton. Strict separation.
• geometric_hahn_banach_point_point: Both sets are singletons. Strict separation.

## TODO #

• Eidelheit's theorem
• Convex ℝ s → interior (closure s) ⊆ s
theorem separate_convex_open_set {E : Type u_2} [] [] [] [] {s : Set E} (hs₀ : 0 s) (hs₁ : ) (hs₂ : ) {x₀ : E} (hx₀ : ¬x₀ s) :
f, f x₀ = 1 ∀ (x : E), x sf x < 1

Given a set s which is a convex neighbourhood of 0 and a point x₀ outside of it, there is a continuous linear functional f separating x₀ and s, in the sense that it sends x₀ to 1 and all of s to values strictly below 1.

theorem geometric_hahn_banach_open {E : Type u_2} [] [] [] [] {s : Set E} {t : Set E} (hs₁ : ) (hs₂ : ) (ht : ) (disj : Disjoint s t) :
f u, (∀ (a : E), a sf a < u) ∀ (b : E), b tu f b

A version of the Hahn-Banach theorem: given disjoint convex sets s, t where s is open, there is a continuous linear functional which separates them.

theorem geometric_hahn_banach_open_point {E : Type u_2} [] [] [] [] {s : Set E} {x : E} (hs₁ : ) (hs₂ : ) (disj : ¬x s) :
f, ∀ (a : E), a sf a < f x
theorem geometric_hahn_banach_point_open {E : Type u_2} [] [] [] [] {t : Set E} {x : E} (ht₁ : ) (ht₂ : ) (disj : ¬x t) :
f, ∀ (b : E), b tf x < f b
theorem geometric_hahn_banach_open_open {E : Type u_2} [] [] [] [] {s : Set E} {t : Set E} (hs₁ : ) (hs₂ : ) (ht₁ : ) (ht₃ : ) (disj : Disjoint s t) :
f u, (∀ (a : E), a sf a < u) ∀ (b : E), b tu < f b
theorem geometric_hahn_banach_compact_closed {E : Type u_2} [] [] [] [] {s : Set E} {t : Set E} [] (hs₁ : ) (hs₂ : ) (ht₁ : ) (ht₂ : ) (disj : Disjoint s t) :
f u v, (∀ (a : E), a sf a < u) u < v ∀ (b : E), b tv < f b

A version of the Hahn-Banach theorem: given disjoint convex sets s, t where s is compact and t is closed, there is a continuous linear functional which strongly separates them.

theorem geometric_hahn_banach_closed_compact {E : Type u_2} [] [] [] [] {s : Set E} {t : Set E} [] (hs₁ : ) (hs₂ : ) (ht₁ : ) (ht₂ : ) (disj : Disjoint s t) :
f u v, (∀ (a : E), a sf a < u) u < v ∀ (b : E), b tv < f b

A version of the Hahn-Banach theorem: given disjoint convex sets s, t where s is closed, and t is compact, there is a continuous linear functional which strongly separates them.

theorem geometric_hahn_banach_point_closed {E : Type u_2} [] [] [] [] {t : Set E} {x : E} [] (ht₁ : ) (ht₂ : ) (disj : ¬x t) :
f u, f x < u ∀ (b : E), b tu < f b
theorem geometric_hahn_banach_closed_point {E : Type u_2} [] [] [] [] {s : Set E} {x : E} [] (hs₁ : ) (hs₂ : ) (disj : ¬x s) :
f u, (∀ (a : E), a sf a < u) u < f x
theorem geometric_hahn_banach_point_point {E : Type u_2} [] [] [] [] {x : E} {y : E} [] [] (hxy : x y) :
f, f x < f y

See also NormedSpace.eq_iff_forall_dual_eq.

theorem iInter_halfspaces_eq {E : Type u_2} [] [] [] [] {s : Set E} [] (hs₁ : ) (hs₂ : ) :
⋂ (l : ), {x | y, y s l x l y} = s

A closed convex set is the intersection of the halfspaces containing it.