Commit 2023-03-29 10:04 be0f2880

View on Github →

feat: port Analysis.Convex.Extreme (#3167)

Estimated changes

Modified Mathlib.lean

Created Mathlib/Analysis/Convex/Extreme.lean

added theorem Convex.mem_extremePoints_iff_convex_diff

added theorem Convex.mem_extremePoints_iff_mem_diff_convexHull_diff

added theorem IsExtreme.convex_diff

added theorem IsExtreme.extremePoints_eq

added theorem IsExtreme.extremePoints_subset_extremePoints

added theorem IsExtreme.inter

added def IsExtreme

added def Set.extremePoints

added theorem extremePoints_convexHull_subset

added theorem extremePoints_empty

added theorem extremePoints_pi

added theorem extremePoints_prod

added theorem extremePoints_singleton

added theorem extremePoints_subset

added theorem inter_extremePoints_subset_extremePoints_of_subset

added theorem isExtreme_binterᵢ

added theorem isExtreme_interᵢ

added theorem isExtreme_interₛ

added theorem mem_extremePoints

added theorem mem_extremePoints_iff_extreme_singleton

added theorem mem_extremePoints_iff_forall_segment