Commit 2023-05-25 08:46 01cfa4d5

View on Github →

feat: port Analysis.NormedSpace.HahnBanach.Separation (#4317)

Estimated changes

Modified Mathlib.lean

Created Mathlib/Analysis/NormedSpace/HahnBanach/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 iInter_halfspaces_eq

added theorem separate_convex_open_set