Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2022-10-27 05:32 bcf8d82b

View on Github →

feat(analysis/normed_space/hahn_banach/separation): generalize to (locally convex) topological vector spaces (#16796)

Estimated changes

Modified src/analysis/convex/exposed.lean

Modified src/analysis/convex/gauge.lean

added theorem gauge_neg_set_eq_gauge_neg

added theorem gauge_neg_set_neg

Modified src/analysis/convex/krein_milman.lean

Modified src/analysis/normed_space/hahn_banach/separation.lean

modified theorem geometric_hahn_banach_point_point

modified theorem separate_convex_open_set

Modified src/topology/algebra/const_mul_action.lean

added theorem dense.smul