Mathlib v3 is deprecated. Go to Mathlib v4

Theorem separate_convex_open_set

Modification history

2022-10-27 05:32
src/analysis/normed_space/hahn_banach/separation.lean
feat(analysis/normed_space/hahn_banach/separation): generalize to (locally convex) topological vector spaces (#16796)
Modified separate_convex_open_setView on Github →
2022-07-24 16:34
src/analysis/normed_space/hahn_banach/separation.lean
chore(*): Rename `normed_group` to `normed_add_comm_group` (#15619) …
Modified separate_convex_open_setView on Github →
2022-05-29 13:40
src/analysis/normed_space/hahn_banach/separation.lean
feat(analysis/normed_space): Geometric Hahn Banach theorems (#7288) …
Added separate_convex_open_setView on Github →