Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2021-06-18 13:40 7c9a8113

View on Github →

feat(analysis/convex/basic): missing lemmas (#7946)

  • the union of a set/indexed family of convex sets is convex
  • open_segment a b is convex
  • a set is nonempty iff its convex hull is

Estimated changes

modified theorem convex_Inter
added theorem convex_open_segment
added theorem directed.convex_Union