Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2021-10-01 17:21 db6d8627

View on Github →

split(analysis/convex/basic): split off analysis.convex.hull (#9477)

Estimated changes

Modified src/analysis/convex/basic.lean

deleted theorem affine_map.image_convex_hull

deleted theorem convex.convex_hull_eq

deleted theorem convex.convex_remove_iff_not_mem_convex_hull_remove

deleted theorem convex_convex_hull

deleted def convex_hull

deleted theorem convex_hull_empty

deleted theorem convex_hull_empty_iff

deleted theorem convex_hull_min

deleted theorem convex_hull_mono

deleted theorem convex_hull_nonempty_iff

deleted theorem convex_hull_singleton

deleted theorem is_linear_map.convex_hull_image

deleted theorem is_linear_map.image_convex_hull

deleted theorem linear_map.convex_hull_image

deleted theorem linear_map.image_convex_hull

deleted theorem subset_convex_hull

Modified src/analysis/convex/combination.lean

Modified src/analysis/convex/cone.lean

Modified src/analysis/convex/extreme.lean

Created src/analysis/convex/hull.lean

added theorem affine_map.image_convex_hull

added theorem convex.convex_hull_eq

added theorem convex.convex_remove_iff_not_mem_convex_hull_remove

added theorem convex_convex_hull

added def convex_hull

added theorem convex_hull_empty

added theorem convex_hull_empty_iff

added theorem convex_hull_min

added theorem convex_hull_mono

added theorem convex_hull_nonempty_iff

added theorem convex_hull_singleton

added theorem is_linear_map.convex_hull_image

added theorem is_linear_map.image_convex_hull

added theorem linear_map.convex_hull_image

added theorem linear_map.image_convex_hull

added theorem subset_convex_hull