Commit 2023-04-25 20:39 262e026d

View on Github →

feat: port Analysis.Convex.Join (#3633)

Estimated changes

Modified Mathlib.lean

Modified Mathlib/Analysis/Convex/Basic.lean

added theorem Convex.exists_mem_add_smul_eq

Modified Mathlib/Analysis/Convex/Hull.lean

modified theorem AffineMap.image_convexHull

Created Mathlib/Analysis/Convex/Join.lean

added theorem convexHull_insert

added theorem convexHull_union

added def convexJoin

added theorem convexJoin_assoc

added theorem convexJoin_assoc_aux

added theorem convexJoin_comm

added theorem convexJoin_convexJoin_convexJoin_comm

added theorem convexJoin_empty_left

added theorem convexJoin_empty_right

added theorem convexJoin_left_comm

added theorem convexJoin_mono

added theorem convexJoin_mono_left

added theorem convexJoin_mono_right

added theorem convexJoin_right_comm

added theorem convexJoin_segment_singleton

added theorem convexJoin_segments

added theorem convexJoin_singleton_left

added theorem convexJoin_singleton_right

added theorem convexJoin_singleton_segment

added theorem convexJoin_singletons

added theorem convexJoin_subset

added theorem convexJoin_subset_convexHull

added theorem convexJoin_union_left

added theorem convexJoin_union_right

added theorem convexJoin_unionᵢ_left

added theorem convexJoin_unionᵢ_right

added theorem mem_convexJoin

added theorem segment_subset_convexJoin

added theorem subset_convexJoin_left

added theorem subset_convexJoin_right

Modified Mathlib/Data/Set/Pointwise/SMul.lean

added theorem Set.add_smul_subset