Star-convex sets

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, Star and co.

Main declarations

• StarConvex 𝕜 x s: s is star-convex at x with 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 StarConvex (𝕜 : Type u_1) {E : Type u_2} [OrderedSemiring 𝕜] [AddCommMonoid E] [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.

Equations

• StarConvex 𝕜 x s = ∀ ⦃y : E⦄, y ∈ s → ∀ ⦃a b : 𝕜⦄, 0 ≤ a → 0 ≤ b → a + b = 1 → a • x + b • y ∈ s

theorem starConvex_iff_segment_subset {𝕜 : Type u_1} {E : Type u_2} [OrderedSemiring 𝕜] [AddCommMonoid E] [SMul 𝕜 E] {x : E} {s : Set E} : StarConvex 𝕜 x s ↔ ∀ ⦃y : E⦄, y ∈ s → segment 𝕜 x y ⊆ s

theorem StarConvex.segment_subset {𝕜 : Type u_1} {E : Type u_2} [OrderedSemiring 𝕜] [AddCommMonoid E] [SMul 𝕜 E] {x : E} {s : Set E} (h : StarConvex 𝕜 x s) {y : E} (hy : y ∈ s) : segment 𝕜 x y ⊆ s

theorem StarConvex.openSegment_subset {𝕜 : Type u_1} {E : Type u_2} [OrderedSemiring 𝕜] [AddCommMonoid E] [SMul 𝕜 E] {x : E} {s : Set E} (h : StarConvex 𝕜 x s) {y : E} (hy : y ∈ s) : openSegment 𝕜 x y ⊆ s

theorem starConvex_iff_pointwise_add_subset {𝕜 : Type u_1} {E : Type u_2} [OrderedSemiring 𝕜] [AddCommMonoid E] [SMul 𝕜 E] {x : E} {s : Set E} : StarConvex 𝕜 x s ↔ ∀ ⦃a b : 𝕜⦄, 0 ≤ a → 0 ≤ b → a + b = 1 → a • {x} + b • s ⊆ s

Alternative definition of star-convexity, in terms of pointwise set operations.

theorem starConvex_empty {𝕜 : Type u_1} {E : Type u_2} [OrderedSemiring 𝕜] [AddCommMonoid E] [SMul 𝕜 E] (x : E) : StarConvex 𝕜 x ∅

theorem starConvex_univ {𝕜 : Type u_1} {E : Type u_2} [OrderedSemiring 𝕜] [AddCommMonoid E] [SMul 𝕜 E] (x : E) : StarConvex 𝕜 x Set.univ

theorem StarConvex.inter {𝕜 : Type u_1} {E : Type u_2} [OrderedSemiring 𝕜] [AddCommMonoid E] [SMul 𝕜 E] {x : E} {s t : Set E} (hs : StarConvex 𝕜 x s) (ht : StarConvex 𝕜 x t) : StarConvex 𝕜 x (s ∩ t)

theorem starConvex_sInter {𝕜 : Type u_1} {E : Type u_2} [OrderedSemiring 𝕜] [AddCommMonoid E] [SMul 𝕜 E] {x : E} {S : Set (Set E)} (h : ∀ s ∈ S, StarConvex 𝕜 x s) : StarConvex 𝕜 x (⋂₀ S)

theorem starConvex_iInter {𝕜 : Type u_1} {E : Type u_2} [OrderedSemiring 𝕜] [AddCommMonoid E] [SMul 𝕜 E] {x : E} {ι : Sort u_4} {s : ι → Set E} (h : ∀ (i : ι), StarConvex 𝕜 x (s i)) : StarConvex 𝕜 x (⋂ (i : ι), s i)

theorem StarConvex.union {𝕜 : Type u_1} {E : Type u_2} [OrderedSemiring 𝕜] [AddCommMonoid E] [SMul 𝕜 E] {x : E} {s t : Set E} (hs : StarConvex 𝕜 x s) (ht : StarConvex 𝕜 x t) : StarConvex 𝕜 x (s ∪ t)

theorem starConvex_iUnion {𝕜 : Type u_1} {E : Type u_2} [OrderedSemiring 𝕜] [AddCommMonoid E] [SMul 𝕜 E] {x : E} {ι : Sort u_4} {s : ι → Set E} (hs : ∀ (i : ι), StarConvex 𝕜 x (s i)) : StarConvex 𝕜 x (⋃ (i : ι), s i)

theorem starConvex_sUnion {𝕜 : Type u_1} {E : Type u_2} [OrderedSemiring 𝕜] [AddCommMonoid E] [SMul 𝕜 E] {x : E} {S : Set (Set E)} (hS : ∀ s ∈ S, StarConvex 𝕜 x s) : StarConvex 𝕜 x (⋃₀ S)

theorem StarConvex.prod {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [OrderedSemiring 𝕜] [AddCommMonoid E] [AddCommMonoid F] [SMul 𝕜 E] [SMul 𝕜 F] {x : E} {y : F} {s : Set E} {t : Set F} (hs : StarConvex 𝕜 x s) (ht : StarConvex 𝕜 y t) : StarConvex 𝕜 (x, y) (s ×ˢ t)

theorem starConvex_pi {𝕜 : Type u_1} [OrderedSemiring 𝕜] {ι : Type u_4} {E : ι → Type u_5} [(i : ι) → AddCommMonoid (E i)] [(i : ι) → SMul 𝕜 (E i)] {x : (i : ι) → E i} {s : Set ι} {t : (i : ι) → Set (E i)} (ht : ∀ ⦃i : ι⦄, i ∈ s → StarConvex 𝕜 (x i) (t i)) : StarConvex 𝕜 x (s.pi t)

theorem StarConvex.mem {𝕜 : Type u_1} {E : Type u_2} [OrderedSemiring 𝕜] [AddCommMonoid E] [Module 𝕜 E] {x : E} {s : Set E} (hs : StarConvex 𝕜 x s) (h : s.Nonempty) : x ∈ s

theorem starConvex_iff_forall_pos {𝕜 : Type u_1} {E : Type u_2} [OrderedSemiring 𝕜] [AddCommMonoid E] [Module 𝕜 E] {x : E} {s : Set E} (hx : x ∈ s) : StarConvex 𝕜 x s ↔ ∀ ⦃y : E⦄, y ∈ s → ∀ ⦃a b : 𝕜⦄, 0 < a → 0 < b → a + b = 1 → a • x + b • y ∈ s

theorem starConvex_iff_forall_ne_pos {𝕜 : Type u_1} {E : Type u_2} [OrderedSemiring 𝕜] [AddCommMonoid E] [Module 𝕜 E] {x : E} {s : Set E} (hx : x ∈ s) : StarConvex 𝕜 x s ↔ ∀ ⦃y : E⦄, y ∈ s → x ≠ y → ∀ ⦃a b : 𝕜⦄, 0 < a → 0 < b → a + b = 1 → a • x + b • y ∈ s

theorem starConvex_iff_openSegment_subset {𝕜 : Type u_1} {E : Type u_2} [OrderedSemiring 𝕜] [AddCommMonoid E] [Module 𝕜 E] {x : E} {s : Set E} (hx : x ∈ s) : StarConvex 𝕜 x s ↔ ∀ ⦃y : E⦄, y ∈ s → openSegment 𝕜 x y ⊆ s

theorem starConvex_singleton {𝕜 : Type u_1} {E : Type u_2} [OrderedSemiring 𝕜] [AddCommMonoid E] [Module 𝕜 E] (x : E) : StarConvex 𝕜 x {x}

theorem StarConvex.linear_image {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [OrderedSemiring 𝕜] [AddCommMonoid E] [AddCommMonoid F] [Module 𝕜 E] [Module 𝕜 F] {x : E} {s : Set E} (hs : StarConvex 𝕜 x s) (f : E →ₗ[𝕜] F) : StarConvex 𝕜 (f x) (⇑f '' s)

theorem StarConvex.is_linear_image {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [OrderedSemiring 𝕜] [AddCommMonoid E] [AddCommMonoid F] [Module 𝕜 E] [Module 𝕜 F] {x : E} {s : Set E} (hs : StarConvex 𝕜 x s) {f : E → F} (hf : IsLinearMap 𝕜 f) : StarConvex 𝕜 (f x) (f '' s)

theorem StarConvex.linear_preimage {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [OrderedSemiring 𝕜] [AddCommMonoid E] [AddCommMonoid F] [Module 𝕜 E] [Module 𝕜 F] {x : E} {s : Set F} (f : E →ₗ[𝕜] F) (hs : StarConvex 𝕜 (f x) s) : StarConvex 𝕜 x (⇑f ⁻¹' s)

theorem StarConvex.is_linear_preimage {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [OrderedSemiring 𝕜] [AddCommMonoid E] [AddCommMonoid F] [Module 𝕜 E] [Module 𝕜 F] {x : E} {s : Set F} {f : E → F} (hs : StarConvex 𝕜 (f x) s) (hf : IsLinearMap 𝕜 f) : StarConvex 𝕜 x (f ⁻¹' s)

theorem StarConvex.add {𝕜 : Type u_1} {E : Type u_2} [OrderedSemiring 𝕜] [AddCommMonoid E] [Module 𝕜 E] {x y : E} {s t : Set E} (hs : StarConvex 𝕜 x s) (ht : StarConvex 𝕜 y t) : StarConvex 𝕜 (x + y) (s + t)

theorem StarConvex.add_left {𝕜 : Type u_1} {E : Type u_2} [OrderedSemiring 𝕜] [AddCommMonoid E] [Module 𝕜 E] {x : E} {s : Set E} (hs : StarConvex 𝕜 x s) (z : E) : StarConvex 𝕜 (z + x) ((fun (x : E) => z + x) '' s)

theorem StarConvex.add_right {𝕜 : Type u_1} {E : Type u_2} [OrderedSemiring 𝕜] [AddCommMonoid E] [Module 𝕜 E] {x : E} {s : Set E} (hs : StarConvex 𝕜 x s) (z : E) : StarConvex 𝕜 (x + z) ((fun (x : E) => x + z) '' s)

theorem StarConvex.preimage_add_right {𝕜 : Type u_1} {E : Type u_2} [OrderedSemiring 𝕜] [AddCommMonoid E] [Module 𝕜 E] {x z : E} {s : Set E} (hs : StarConvex 𝕜 (z + x) s) : StarConvex 𝕜 x ((fun (x : E) => z + x) ⁻¹' s)

The translation of a star-convex set is also star-convex.

theorem StarConvex.preimage_add_left {𝕜 : Type u_1} {E : Type u_2} [OrderedSemiring 𝕜] [AddCommMonoid E] [Module 𝕜 E] {x z : E} {s : Set E} (hs : StarConvex 𝕜 (x + z) s) : StarConvex 𝕜 x ((fun (x : E) => x + z) ⁻¹' s)

The translation of a star-convex set is also star-convex.

theorem StarConvex.sub' {𝕜 : Type u_1} {E : Type u_2} [OrderedSemiring 𝕜] [AddCommGroup E] [Module 𝕜 E] {x y : E} {s : Set (E × E)} (hs : StarConvex 𝕜 (x, y) s) : StarConvex 𝕜 (x - y) ((fun (x : E × E) => x.1 - x.2) '' s)

theorem StarConvex.smul {𝕜 : Type u_1} {E : Type u_2} [OrderedCommSemiring 𝕜] [AddCommMonoid E] [Module 𝕜 E] {x : E} {s : Set E} (hs : StarConvex 𝕜 x s) (c : 𝕜) : StarConvex 𝕜 (c • x) (c • s)

theorem StarConvex.preimage_smul {𝕜 : Type u_1} {E : Type u_2} [OrderedCommSemiring 𝕜] [AddCommMonoid E] [Module 𝕜 E] {x : E} {s : Set E} {c : 𝕜} (hs : StarConvex 𝕜 (c • x) s) : StarConvex 𝕜 x ((fun (z : E) => c • z) ⁻¹' s)

theorem StarConvex.affinity {𝕜 : Type u_1} {E : Type u_2} [OrderedCommSemiring 𝕜] [AddCommMonoid E] [Module 𝕜 E] {x : E} {s : Set E} (hs : StarConvex 𝕜 x s) (z : E) (c : 𝕜) : StarConvex 𝕜 (z + c • x) ((fun (x : E) => z + c • x) '' s)

theorem starConvex_zero_iff {𝕜 : Type u_1} {E : Type u_2} [OrderedRing 𝕜] [AddCommMonoid E] [SMulWithZero 𝕜 E] {s : Set E} : StarConvex 𝕜 0 s ↔ ∀ ⦃x : E⦄, x ∈ s → ∀ ⦃a : 𝕜⦄, 0 ≤ a → a ≤ 1 → a • x ∈ s

theorem StarConvex.add_smul_mem {𝕜 : Type u_1} {E : Type u_2} [OrderedRing 𝕜] [AddCommGroup E] [Module 𝕜 E] {x y : E} {s : Set E} (hs : StarConvex 𝕜 x s) (hy : x + y ∈ s) {t : 𝕜} (ht₀ : 0 ≤ t) (ht₁ : t ≤ 1) : x + t • y ∈ s

theorem StarConvex.smul_mem {𝕜 : Type u_1} {E : Type u_2} [OrderedRing 𝕜] [AddCommGroup E] [Module 𝕜 E] {x : E} {s : Set E} (hs : StarConvex 𝕜 0 s) (hx : x ∈ s) {t : 𝕜} (ht₀ : 0 ≤ t) (ht₁ : t ≤ 1) : t • x ∈ s

theorem StarConvex.add_smul_sub_mem {𝕜 : Type u_1} {E : Type u_2} [OrderedRing 𝕜] [AddCommGroup E] [Module 𝕜 E] {x y : E} {s : Set E} (hs : StarConvex 𝕜 x s) (hy : y ∈ s) {t : 𝕜} (ht₀ : 0 ≤ t) (ht₁ : t ≤ 1) : x + t • (y - x) ∈ s

theorem StarConvex.affine_preimage {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [OrderedRing 𝕜] [AddCommGroup E] [AddCommGroup F] [Module 𝕜 E] [Module 𝕜 F] {x : E} (f : E →ᵃ[𝕜] F) {s : Set F} (hs : StarConvex 𝕜 (f x) s) : StarConvex 𝕜 x (⇑f ⁻¹' s)

The preimage of a star-convex set under an affine map is star-convex.

theorem StarConvex.affine_image {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [OrderedRing 𝕜] [AddCommGroup E] [AddCommGroup F] [Module 𝕜 E] [Module 𝕜 F] {x : E} (f : E →ᵃ[𝕜] F) {s : Set E} (hs : StarConvex 𝕜 x s) : StarConvex 𝕜 (f x) (⇑f '' s)

The image of a star-convex set under an affine map is star-convex.

theorem StarConvex.neg {𝕜 : Type u_1} {E : Type u_2} [OrderedRing 𝕜] [AddCommGroup E] [Module 𝕜 E] {x : E} {s : Set E} (hs : StarConvex 𝕜 x s) : StarConvex 𝕜 (-x) (-s)

theorem StarConvex.sub {𝕜 : Type u_1} {E : Type u_2} [OrderedRing 𝕜] [AddCommGroup E] [Module 𝕜 E] {x y : E} {s t : Set E} (hs : StarConvex 𝕜 x s) (ht : StarConvex 𝕜 y t) : StarConvex 𝕜 (x - y) (s - t)

theorem starConvex_compl_Iic {𝕜 : Type u_1} {E : Type u_2} [OrderedRing 𝕜] [OrderedAddCommGroup E] [Module 𝕜 E] [OrderedSMul 𝕜 E] {x y : E} (h : x < y) : StarConvex 𝕜 y (Set.Iic x)ᶜ

If x < y, then (Set.Iic x)ᶜ is star convex at y.

theorem starConvex_compl_Ici {𝕜 : Type u_1} {E : Type u_2} [OrderedRing 𝕜] [OrderedAddCommGroup E] [Module 𝕜 E] [OrderedSMul 𝕜 E] {x y : E} (h : x < y) : StarConvex 𝕜 x (Set.Ici y)ᶜ

If x < y, then (Set.Ici y)ᶜ is star convex at x.

theorem starConvex_iff_div {𝕜 : Type u_1} {E : Type u_2} [LinearOrderedField 𝕜] [AddCommGroup E] [Module 𝕜 E] {x : E} {s : Set E} : StarConvex 𝕜 x s ↔ ∀ ⦃y : E⦄, y ∈ s → ∀ ⦃a b : 𝕜⦄, 0 ≤ a → 0 ≤ b → 0 < a + b → (a / (a + b)) • x + (b / (a + b)) • y ∈ s

Alternative definition of star-convexity, using division.

theorem StarConvex.mem_smul {𝕜 : Type u_1} {E : Type u_2} [LinearOrderedField 𝕜] [AddCommGroup E] [Module 𝕜 E] {x : E} {s : Set E} (hs : StarConvex 𝕜 0 s) (hx : x ∈ s) {t : 𝕜} (ht : 1 ≤ t) : x ∈ t • s

Star-convex sets in an ordered space

Relates starConvex and Set.ordConnected.

theorem Set.OrdConnected.starConvex {𝕜 : Type u_1} {E : Type u_2} [OrderedSemiring 𝕜] [OrderedAddCommMonoid E] [Module 𝕜 E] [OrderedSMul 𝕜 E] {x : E} {s : Set E} (hs : s.OrdConnected) (hx : x ∈ s) (h : ∀ y ∈ s, x ≤ y ∨ y ≤ x) : StarConvex 𝕜 x s

If s is an order-connected set in an ordered module over an ordered semiring and all elements of s are comparable with x ∈ s, then s is StarConvex at x.

theorem starConvex_iff_ordConnected {𝕜 : Type u_1} [LinearOrderedField 𝕜] {x : 𝕜} {s : Set 𝕜} (hx : x ∈ s) : StarConvex 𝕜 x s ↔ s.OrdConnected

theorem StarConvex.ordConnected {𝕜 : Type u_1} [LinearOrderedField 𝕜] {x : 𝕜} {s : Set 𝕜} (hx : x ∈ s) : StarConvex 𝕜 x s → s.OrdConnected

Alias of the forward direction of starConvex_iff_ordConnected.