Commit 2023-04-17 08:52 7e4c9ba7

View on Github →

feat: port Analysis.Convex.Exposed (#3453)

Estimated changes

Modified Mathlib.lean

Created Mathlib/Analysis/Convex/Exposed.lean

added theorem ContinuousLinearMap.toExposed.isExposed

added def ContinuousLinearMap.toExposed

added theorem IsExposed.eq_inter_halfspace'

added theorem IsExposed.eq_inter_halfspace

added theorem IsExposed.inter_left

added theorem IsExposed.inter_right

added theorem IsExposed.interₛ

added def IsExposed

added def Set.exposedPoints

added theorem exposedPoints_empty

added theorem exposedPoints_subset

added theorem exposedPoints_subset_extremePoints

added theorem exposed_point_def

added theorem isExposed_empty

added theorem mem_exposedPoints_iff_exposed_singleton