Mathlib v3 is deprecated. Go to Mathlib v4

Theorem geometric_hahn_banach_point_point

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 geometric_hahn_banach_point_pointView 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 geometric_hahn_banach_point_pointView on Github →