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.