Commit 2024-08-02 21:35 2f5275c4

View on Github →

feat: RCLike versions of Hahn-Banach separation theorems (#15416) Generalized first definition in Mathlib.Analysis.NormedSpace.Extend, and used this to prove RCLike generalizations of Hahn-Banach separation theorems.

Estimated changes

Modified Mathlib/Analysis/NormedSpace/Extend.lean

Modified Mathlib/Analysis/NormedSpace/HahnBanach/Separation.lean

added theorem RCLike.geometric_hahn_banach_closed_compact

added theorem RCLike.geometric_hahn_banach_closed_point

added theorem RCLike.geometric_hahn_banach_compact_closed

added theorem RCLike.geometric_hahn_banach_open

added theorem RCLike.geometric_hahn_banach_open_open

added theorem RCLike.geometric_hahn_banach_open_point

added theorem RCLike.geometric_hahn_banach_point_closed

added theorem RCLike.geometric_hahn_banach_point_open

added theorem RCLike.geometric_hahn_banach_point_point

added theorem RCLike.iInter_halfspaces_eq

added theorem RCLike.re_extendTo𝕜'ₗ

added theorem RCLike.separate_convex_open_set