Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2022-05-29 13:40 b673ed8a

View on Github →

feat(analysis/normed_space): Geometric Hahn Banach theorems (#7288) This proves a range of variants of the Hahn-Banach separation theorems.

Estimated changes

Modified counterexamples/phillips.lean

Modified src/analysis/normed_space/dual.lean

Renamed src/analysis/normed_space/hahn_banach.lean to src/analysis/normed_space/hahn_banach/extension.lean

Created src/analysis/normed_space/hahn_banach/separation.lean

added theorem geometric_hahn_banach_closed_compact

added theorem geometric_hahn_banach_closed_point

added theorem geometric_hahn_banach_compact_closed

added theorem geometric_hahn_banach_open

added theorem geometric_hahn_banach_open_open

added theorem geometric_hahn_banach_open_point

added theorem geometric_hahn_banach_point_closed

added theorem geometric_hahn_banach_point_open

added theorem geometric_hahn_banach_point_point

added theorem separate_convex_open_set

Modified src/data/set/pointwise.lean