Star-convex sets #
THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.
This files defines star-convex sets (aka star domains, star-shaped set, radially convex set).
A set is star-convex at x if every segment from x to a point in the set is contained in the set.
This is the prototypical example of a contractible set in homotopy theory (by scaling every point
towards x), but has wider uses.
Note that this has nothing to do with star rings, has_star and co.
Main declarations #
star_convex 𝕜 x s:sis star-convex atxwith scalars𝕜.
Implementation notes #
Instead of saying that a set is star-convex, we say a set is star-convex at a point. This has the advantage of allowing us to talk about convexity as being "everywhere star-convexity" and of making the union of star-convex sets be star-convex.
Incidentally, this choice means we don't need to assume a set is nonempty for it to be star-convex. Concretely, the empty set is star-convex at every point.
TODO #
Balanced sets are star-convex.
The closure of a star-convex set is star-convex.
Star-convex sets are contractible.
A nonempty open star-convex set in ℝ^n is diffeomorphic to the entire space.
def
star_convex
(𝕜 : Type u_1)
{E : Type u_2}
[ordered_semiring 𝕜]
[add_comm_monoid E]
[has_smul 𝕜 E]
(x : E)
(s : set E) :
Prop
Star-convexity of sets. s is star-convex at x if every segment from x to a point in s is
contained in s.
theorem
star_convex_iff_segment_subset
{𝕜 : Type u_1}
{E : Type u_2}
[ordered_semiring 𝕜]
[add_comm_monoid E]
[has_smul 𝕜 E]
{x : E}
{s : set E} :
theorem
star_convex.segment_subset
{𝕜 : Type u_1}
{E : Type u_2}
[ordered_semiring 𝕜]
[add_comm_monoid E]
[has_smul 𝕜 E]
{x : E}
{s : set E}
(h : star_convex 𝕜 x s)
{y : E}
(hy : y ∈ s) :
theorem
star_convex.open_segment_subset
{𝕜 : Type u_1}
{E : Type u_2}
[ordered_semiring 𝕜]
[add_comm_monoid E]
[has_smul 𝕜 E]
{x : E}
{s : set E}
(h : star_convex 𝕜 x s)
{y : E}
(hy : y ∈ s) :
open_segment 𝕜 x y ⊆ s
theorem
star_convex_iff_pointwise_add_subset
{𝕜 : Type u_1}
{E : Type u_2}
[ordered_semiring 𝕜]
[add_comm_monoid E]
[has_smul 𝕜 E]
{x : E}
{s : set E} :
Alternative definition of star-convexity, in terms of pointwise set operations.
theorem
star_convex_empty
{𝕜 : Type u_1}
{E : Type u_2}
[ordered_semiring 𝕜]
[add_comm_monoid E]
[has_smul 𝕜 E]
(x : E) :
star_convex 𝕜 x ∅
theorem
star_convex_univ
{𝕜 : Type u_1}
{E : Type u_2}
[ordered_semiring 𝕜]
[add_comm_monoid E]
[has_smul 𝕜 E]
(x : E) :
star_convex 𝕜 x set.univ
theorem
star_convex.inter
{𝕜 : Type u_1}
{E : Type u_2}
[ordered_semiring 𝕜]
[add_comm_monoid E]
[has_smul 𝕜 E]
{x : E}
{s t : set E}
(hs : star_convex 𝕜 x s)
(ht : star_convex 𝕜 x t) :
star_convex 𝕜 x (s ∩ t)
theorem
star_convex_sInter
{𝕜 : Type u_1}
{E : Type u_2}
[ordered_semiring 𝕜]
[add_comm_monoid E]
[has_smul 𝕜 E]
{x : E}
{S : set (set E)}
(h : ∀ (s : set E), s ∈ S → star_convex 𝕜 x s) :
star_convex 𝕜 x (⋂₀ S)
theorem
star_convex_Inter
{𝕜 : Type u_1}
{E : Type u_2}
[ordered_semiring 𝕜]
[add_comm_monoid E]
[has_smul 𝕜 E]
{x : E}
{ι : Sort u_3}
{s : ι → set E}
(h : ∀ (i : ι), star_convex 𝕜 x (s i)) :
star_convex 𝕜 x (⋂ (i : ι), s i)
theorem
star_convex.union
{𝕜 : Type u_1}
{E : Type u_2}
[ordered_semiring 𝕜]
[add_comm_monoid E]
[has_smul 𝕜 E]
{x : E}
{s t : set E}
(hs : star_convex 𝕜 x s)
(ht : star_convex 𝕜 x t) :
star_convex 𝕜 x (s ∪ t)
theorem
star_convex_Union
{𝕜 : Type u_1}
{E : Type u_2}
[ordered_semiring 𝕜]
[add_comm_monoid E]
[has_smul 𝕜 E]
{x : E}
{ι : Sort u_3}
{s : ι → set E}
(hs : ∀ (i : ι), star_convex 𝕜 x (s i)) :
star_convex 𝕜 x (⋃ (i : ι), s i)
theorem
star_convex_sUnion
{𝕜 : Type u_1}
{E : Type u_2}
[ordered_semiring 𝕜]
[add_comm_monoid E]
[has_smul 𝕜 E]
{x : E}
{S : set (set E)}
(hS : ∀ (s : set E), s ∈ S → star_convex 𝕜 x s) :
star_convex 𝕜 x (⋃₀ S)
theorem
star_convex.prod
{𝕜 : Type u_1}
{E : Type u_2}
{F : Type u_3}
[ordered_semiring 𝕜]
[add_comm_monoid E]
[add_comm_monoid F]
[has_smul 𝕜 E]
[has_smul 𝕜 F]
{x : E}
{y : F}
{s : set E}
{t : set F}
(hs : star_convex 𝕜 x s)
(ht : star_convex 𝕜 y t) :
star_convex 𝕜 (x, y) (s ×ˢ t)
theorem
star_convex_pi
{𝕜 : Type u_1}
[ordered_semiring 𝕜]
{ι : Type u_2}
{E : ι → Type u_3}
[Π (i : ι), add_comm_monoid (E i)]
[Π (i : ι), has_smul 𝕜 (E i)]
{x : Π (i : ι), E i}
{s : set ι}
{t : Π (i : ι), set (E i)}
(ht : ∀ ⦃i : ι⦄, i ∈ s → star_convex 𝕜 (x i) (t i)) :
star_convex 𝕜 x (s.pi t)
theorem
star_convex.mem
{𝕜 : Type u_1}
{E : Type u_2}
[ordered_semiring 𝕜]
[add_comm_monoid E]
[module 𝕜 E]
{x : E}
{s : set E}
(hs : star_convex 𝕜 x s)
(h : s.nonempty) :
x ∈ s
theorem
star_convex_iff_open_segment_subset
{𝕜 : Type u_1}
{E : Type u_2}
[ordered_semiring 𝕜]
[add_comm_monoid E]
[module 𝕜 E]
{x : E}
{s : set E}
(hx : x ∈ s) :
star_convex 𝕜 x s ↔ ∀ ⦃y : E⦄, y ∈ s → open_segment 𝕜 x y ⊆ s
theorem
star_convex_singleton
{𝕜 : Type u_1}
{E : Type u_2}
[ordered_semiring 𝕜]
[add_comm_monoid E]
[module 𝕜 E]
(x : E) :
star_convex 𝕜 x {x}
theorem
star_convex.linear_image
{𝕜 : Type u_1}
{E : Type u_2}
{F : Type u_3}
[ordered_semiring 𝕜]
[add_comm_monoid E]
[add_comm_monoid F]
[module 𝕜 E]
[module 𝕜 F]
{x : E}
{s : set E}
(hs : star_convex 𝕜 x s)
(f : E →ₗ[𝕜] F) :
star_convex 𝕜 (⇑f x) (⇑f '' s)
theorem
star_convex.is_linear_image
{𝕜 : Type u_1}
{E : Type u_2}
{F : Type u_3}
[ordered_semiring 𝕜]
[add_comm_monoid E]
[add_comm_monoid F]
[module 𝕜 E]
[module 𝕜 F]
{x : E}
{s : set E}
(hs : star_convex 𝕜 x s)
{f : E → F}
(hf : is_linear_map 𝕜 f) :
star_convex 𝕜 (f x) (f '' s)
theorem
star_convex.linear_preimage
{𝕜 : Type u_1}
{E : Type u_2}
{F : Type u_3}
[ordered_semiring 𝕜]
[add_comm_monoid E]
[add_comm_monoid F]
[module 𝕜 E]
[module 𝕜 F]
{x : E}
{s : set F}
(f : E →ₗ[𝕜] F)
(hs : star_convex 𝕜 (⇑f x) s) :
star_convex 𝕜 x (⇑f ⁻¹' s)
theorem
star_convex.is_linear_preimage
{𝕜 : Type u_1}
{E : Type u_2}
{F : Type u_3}
[ordered_semiring 𝕜]
[add_comm_monoid E]
[add_comm_monoid F]
[module 𝕜 E]
[module 𝕜 F]
{x : E}
{s : set F}
{f : E → F}
(hs : star_convex 𝕜 (f x) s)
(hf : is_linear_map 𝕜 f) :
star_convex 𝕜 x (f ⁻¹' s)
theorem
star_convex.add
{𝕜 : Type u_1}
{E : Type u_2}
[ordered_semiring 𝕜]
[add_comm_monoid E]
[module 𝕜 E]
{x y : E}
{s t : set E}
(hs : star_convex 𝕜 x s)
(ht : star_convex 𝕜 y t) :
star_convex 𝕜 (x + y) (s + t)
theorem
star_convex.add_left
{𝕜 : Type u_1}
{E : Type u_2}
[ordered_semiring 𝕜]
[add_comm_monoid E]
[module 𝕜 E]
{x : E}
{s : set E}
(hs : star_convex 𝕜 x s)
(z : E) :
star_convex 𝕜 (z + x) ((λ (x : E), z + x) '' s)
theorem
star_convex.add_right
{𝕜 : Type u_1}
{E : Type u_2}
[ordered_semiring 𝕜]
[add_comm_monoid E]
[module 𝕜 E]
{x : E}
{s : set E}
(hs : star_convex 𝕜 x s)
(z : E) :
star_convex 𝕜 (x + z) ((λ (x : E), x + z) '' s)
theorem
star_convex.preimage_add_right
{𝕜 : Type u_1}
{E : Type u_2}
[ordered_semiring 𝕜]
[add_comm_monoid E]
[module 𝕜 E]
{x z : E}
{s : set E}
(hs : star_convex 𝕜 (z + x) s) :
star_convex 𝕜 x ((λ (x : E), z + x) ⁻¹' s)
The translation of a star-convex set is also star-convex.
theorem
star_convex.preimage_add_left
{𝕜 : Type u_1}
{E : Type u_2}
[ordered_semiring 𝕜]
[add_comm_monoid E]
[module 𝕜 E]
{x z : E}
{s : set E}
(hs : star_convex 𝕜 (x + z) s) :
star_convex 𝕜 x ((λ (x : E), x + z) ⁻¹' s)
The translation of a star-convex set is also star-convex.
theorem
star_convex.sub'
{𝕜 : Type u_1}
{E : Type u_2}
[ordered_semiring 𝕜]
[add_comm_group E]
[module 𝕜 E]
{x y : E}
{s : set (E × E)}
(hs : star_convex 𝕜 (x, y) s) :
theorem
star_convex.smul
{𝕜 : Type u_1}
{E : Type u_2}
[ordered_comm_semiring 𝕜]
[add_comm_monoid E]
[module 𝕜 E]
{x : E}
{s : set E}
(hs : star_convex 𝕜 x s)
(c : 𝕜) :
star_convex 𝕜 (c • x) (c • s)
theorem
star_convex.preimage_smul
{𝕜 : Type u_1}
{E : Type u_2}
[ordered_comm_semiring 𝕜]
[add_comm_monoid E]
[module 𝕜 E]
{x : E}
{s : set E}
{c : 𝕜}
(hs : star_convex 𝕜 (c • x) s) :
star_convex 𝕜 x ((λ (z : E), c • z) ⁻¹' s)
theorem
star_convex.affinity
{𝕜 : Type u_1}
{E : Type u_2}
[ordered_comm_semiring 𝕜]
[add_comm_monoid E]
[module 𝕜 E]
{x : E}
{s : set E}
(hs : star_convex 𝕜 x s)
(z : E)
(c : 𝕜) :
theorem
star_convex_zero_iff
{𝕜 : Type u_1}
{E : Type u_2}
[ordered_ring 𝕜]
[add_comm_monoid E]
[smul_with_zero 𝕜 E]
{s : set E} :
theorem
star_convex.add_smul_mem
{𝕜 : Type u_1}
{E : Type u_2}
[ordered_ring 𝕜]
[add_comm_group E]
[module 𝕜 E]
{x y : E}
{s : set E}
(hs : star_convex 𝕜 x s)
(hy : x + y ∈ s)
{t : 𝕜}
(ht₀ : 0 ≤ t)
(ht₁ : t ≤ 1) :
theorem
star_convex.smul_mem
{𝕜 : Type u_1}
{E : Type u_2}
[ordered_ring 𝕜]
[add_comm_group E]
[module 𝕜 E]
{x : E}
{s : set E}
(hs : star_convex 𝕜 0 s)
(hx : x ∈ s)
{t : 𝕜}
(ht₀ : 0 ≤ t)
(ht₁ : t ≤ 1) :
theorem
star_convex.add_smul_sub_mem
{𝕜 : Type u_1}
{E : Type u_2}
[ordered_ring 𝕜]
[add_comm_group E]
[module 𝕜 E]
{x y : E}
{s : set E}
(hs : star_convex 𝕜 x s)
(hy : y ∈ s)
{t : 𝕜}
(ht₀ : 0 ≤ t)
(ht₁ : t ≤ 1) :
theorem
star_convex.affine_preimage
{𝕜 : Type u_1}
{E : Type u_2}
{F : Type u_3}
[ordered_ring 𝕜]
[add_comm_group E]
[add_comm_group F]
[module 𝕜 E]
[module 𝕜 F]
{x : E}
(f : E →ᵃ[𝕜] F)
{s : set F}
(hs : star_convex 𝕜 (⇑f x) s) :
star_convex 𝕜 x (⇑f ⁻¹' s)
The preimage of a star-convex set under an affine map is star-convex.
theorem
star_convex.affine_image
{𝕜 : Type u_1}
{E : Type u_2}
{F : Type u_3}
[ordered_ring 𝕜]
[add_comm_group E]
[add_comm_group F]
[module 𝕜 E]
[module 𝕜 F]
{x : E}
(f : E →ᵃ[𝕜] F)
{s : set E}
(hs : star_convex 𝕜 x s) :
star_convex 𝕜 (⇑f x) (⇑f '' s)
The image of a star-convex set under an affine map is star-convex.
theorem
star_convex.neg
{𝕜 : Type u_1}
{E : Type u_2}
[ordered_ring 𝕜]
[add_comm_group E]
[module 𝕜 E]
{x : E}
{s : set E}
(hs : star_convex 𝕜 x s) :
star_convex 𝕜 (-x) (-s)
theorem
star_convex.sub
{𝕜 : Type u_1}
{E : Type u_2}
[ordered_ring 𝕜]
[add_comm_group E]
[module 𝕜 E]
{x y : E}
{s t : set E}
(hs : star_convex 𝕜 x s)
(ht : star_convex 𝕜 y t) :
star_convex 𝕜 (x - y) (s - t)
theorem
star_convex_iff_div
{𝕜 : Type u_1}
{E : Type u_2}
[linear_ordered_field 𝕜]
[add_comm_group E]
[module 𝕜 E]
{x : E}
{s : set E} :
Alternative definition of star-convexity, using division.
theorem
star_convex.mem_smul
{𝕜 : Type u_1}
{E : Type u_2}
[linear_ordered_field 𝕜]
[add_comm_group E]
[module 𝕜 E]
{x : E}
{s : set E}
(hs : star_convex 𝕜 0 s)
(hx : x ∈ s)
{t : 𝕜}
(ht : 1 ≤ t) :
Star-convex sets in an ordered space #
Relates star_convex and set.ord_connected.
theorem
set.ord_connected.star_convex
{𝕜 : Type u_1}
{E : Type u_2}
[ordered_semiring 𝕜]
[ordered_add_comm_monoid E]
[module 𝕜 E]
[ordered_smul 𝕜 E]
{x : E}
{s : set E}
(hs : s.ord_connected)
(hx : x ∈ s)
(h : ∀ (y : E), y ∈ s → x ≤ y ∨ y ≤ x) :
star_convex 𝕜 x s
theorem
star_convex_iff_ord_connected
{𝕜 : Type u_1}
[linear_ordered_field 𝕜]
{x : 𝕜}
{s : set 𝕜}
(hx : x ∈ s) :
star_convex 𝕜 x s ↔ s.ord_connected
theorem
star_convex.ord_connected
{𝕜 : Type u_1}
[linear_ordered_field 𝕜]
{x : 𝕜}
{s : set 𝕜}
(hx : x ∈ s) :
star_convex 𝕜 x s → s.ord_connected
Alias of the forward direction of star_convex_iff_ord_connected.