Commit 2023-03-28 12:06 77b0a84b

View on Github →

feat: port Analysis.Convex.Hull (#3147)

Estimated changes

Modified Mathlib.lean

Created Mathlib/Analysis/Convex/Hull.lean

added theorem AffineMap.image_convexHull

added theorem Convex.convexHull_eq

added theorem Convex.convexHull_subset_iff

added theorem Convex.convex_remove_iff_not_mem_convexHull_remove

added theorem IsLinearMap.convexHull_image

added theorem LinearMap.convexHull_image

added theorem affineSpan_convexHull

added def convexHull

added theorem convexHull_convexHull_union_left

added theorem convexHull_convexHull_union_right

added theorem convexHull_empty

added theorem convexHull_empty_iff

added theorem convexHull_eq_interᵢ

added theorem convexHull_min

added theorem convexHull_mono

added theorem convexHull_neg

added theorem convexHull_nonempty_iff

added theorem convexHull_pair

added theorem convexHull_singleton

added theorem convexHull_smul

added theorem convexHull_subset_affineSpan

added theorem convexHull_univ

added theorem convex_convexHull

added theorem mem_convexHull_iff

added theorem segment_subset_convexHull

added theorem subset_convexHull