Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2022-06-20 09:15 04f45054

View on Github →

feat(analysis/convex/join): Join of sets (#14676) Define the join of two sets as the union of all segments between them.

Estimated changes

added theorem convex_hull_pair
modified theorem convex_hull_singleton
added theorem convex_hull_insert
added theorem convex_hull_union
added def convex_join
added theorem convex_join_Union_left
added theorem convex_join_assoc
added theorem convex_join_assoc_aux
added theorem convex_join_comm
added theorem convex_join_empty_left
added theorem convex_join_left_comm
added theorem convex_join_mono
added theorem convex_join_mono_left
added theorem convex_join_mono_right
added theorem convex_join_right_comm
added theorem convex_join_segments
added theorem convex_join_singletons
added theorem convex_join_subset
added theorem convex_join_union_left
added theorem mem_convex_join