Commit 2023-04-25 11:43 b4f2cf60

View on Github →

feat: port Analysis.Convex.Independent (#3641)

Estimated changes

Modified Mathlib.lean

Created Mathlib/Analysis/Convex/Independent.lean

added theorem Convex.convexIndependent_extremePoints

added theorem ConvexIndependent.comp_embedding

added def ConvexIndependent

added theorem Function.Injective.convexIndependent_iff_set

added theorem Subsingleton.convexIndependent

added theorem convexIndependent_iff_finset

added theorem convexIndependent_iff_not_mem_convexHull_diff

added theorem convexIndependent_set_iff_inter_convexHull_subset

added theorem convexIndependent_set_iff_not_mem_convexHull_diff