Commit 2023-05-25 17:59 868ddb6b

View on Github →

feat: port Analysis.Convex.KreinMilman (#4347)

Estimated changes

Modified Mathlib.lean

Created Mathlib/Analysis/Convex/KreinMilman.lean

added theorem IsCompact.has_extreme_point

added theorem closure_convexHull_extremePoints