Commit 2022-05-18 16:04 c38ab356

View on Github →

feat(analysis/convex/combination): The convex hull of s + t (#14160) convex_hull distributes over pointwise addition of sets and commutes with pointwise scalar multiplication. Also delete linear_map.image_convex_hull because it duplicates linear_map.convex_hull_image.

Estimated changes

Modified src/analysis/convex/combination.lean

added theorem convex_hull_add

modified theorem convex_hull_prod

added theorem convex_hull_sub

added theorem mk_mem_convex_hull_prod

Modified src/analysis/convex/hull.lean

modified theorem convex.convex_hull_eq

added theorem convex.convex_hull_subset_iff

added theorem convex_hull_eq_Inter

added theorem convex_hull_neg

added theorem convex_hull_smul

deleted theorem is_linear_map.image_convex_hull

deleted theorem linear_map.image_convex_hull

added theorem mem_convex_hull_iff