Theorem separate_convex_open_set

Modification history

2025-02-16 15:19
Mathlib/Analysis/NormedSpace/HahnBanach/Separation.lean
chore: rename Topological(Semi)Ring -> IsTopological(Semi)Ring and Topological(Add)Group -> IsTopological(Add)Group (#21472)
Modified separate_convex_open_setView on Github →
2023-05-25 08:46
Mathlib/Analysis/NormedSpace/HahnBanach/Separation.lean
feat: port Analysis.NormedSpace.HahnBanach.Separation (#4317)
Added separate_convex_open_setView on Github →