Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2021-09-20 18:11 175afa8a

View on Github →

refactor(analysis/convex/{extreme, exposed}): generalize is_extreme and is_exposed to semimodules (#9264) is_extreme and is_exposed are currently only defined in real vector spaces. This generalizes ℝ to arbitrary ordered_semirings in definitions and abstracts it away to the correct generality in lemmas. It also generalizes the space from add_comm_group to add_comm_monoid.

Estimated changes

modified theorem is_exposed.antisymm
modified theorem is_exposed.inter
modified theorem is_exposed.inter_left
modified theorem is_exposed.inter_right
modified theorem is_exposed.is_closed
modified theorem is_exposed.is_compact
modified theorem is_exposed.refl
modified theorem is_exposed_empty
modified theorem extreme_points_subset
deleted theorem is_extreme.Inter
deleted theorem is_extreme.antisymm
deleted theorem is_extreme.bInter
modified theorem is_extreme.convex_diff
modified theorem is_extreme.inter
deleted theorem is_extreme.mono
deleted theorem is_extreme.refl
deleted theorem is_extreme.sInter
deleted theorem is_extreme.trans
added theorem is_extreme_Inter
added theorem is_extreme_bInter
added theorem is_extreme_sInter