Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2021-12-03 10:55 970f0746

View on Github →

feat(analysis/convex/star): Star-convex sets (#10524) This defines star_convex 𝕜 x s to mean that a set is star-convex (aka star-shaped, radially convex, or a star domain) at x. This means that every segment from x to a point in s is a subset of s.

Estimated changes

added theorem set.set_vadd_singleton
deleted theorem set.vadd_singleton
added theorem set.smul_singleton
modified theorem convex.sub
added theorem convex.star_convex_iff
added theorem star_convex.add
added theorem star_convex.add_left
added theorem star_convex.add_right
added theorem star_convex.affinity
added theorem star_convex.inter
added theorem star_convex.mem
added theorem star_convex.mem_smul
added theorem star_convex.neg
added theorem star_convex.prod
added theorem star_convex.smul
added theorem star_convex.smul_mem
added theorem star_convex.sub
added theorem star_convex.union
added def star_convex
added theorem star_convex_Inter
added theorem star_convex_Union
added theorem star_convex_empty
added theorem star_convex_iff_div
added theorem star_convex_pi
added theorem star_convex_sInter
added theorem star_convex_sUnion
added theorem star_convex_singleton
added theorem star_convex_univ
added theorem submodule.star_convex
added theorem subspace.star_convex
modified theorem set.ord_connected_interval
modified theorem set.not_mem_interval_of_gt
modified theorem set.not_mem_interval_of_lt