Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2021-06-24 15:14 520e79d9

View on Github →

feat(analysis/convex/exposed): introduce exposed sets (#7928) introduce exposed sets

Estimated changes

Created src/analysis/convex/exposed.lean

added theorem continuous_linear_map.to_exposed.is_exposed

added def continuous_linear_map.to_exposed

added theorem exposed_point_def

added theorem exposed_points_empty

added theorem exposed_points_subset

added theorem exposed_points_subset_extreme_points

added theorem is_exposed.antisymm

added theorem is_exposed.eq_inter_halfspace

added theorem is_exposed.inter

added theorem is_exposed.inter_left

added theorem is_exposed.inter_right

added theorem is_exposed.is_closed

added theorem is_exposed.is_compact

added theorem is_exposed.refl

added theorem is_exposed.sInter

added def is_exposed

added theorem is_exposed_empty

added theorem mem_exposed_points_iff_exposed_singleton

added def set.exposed_points

Modified src/analysis/convex/extreme.lean