# 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 ๐] [] [SMul ๐ E] (x : E) (s : Set E) :

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
Instances For
theorem starConvex_iff_segment_subset {๐ : Type u_1} {E : Type u_2} [OrderedSemiring ๐] [] [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 ๐] [] [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 ๐] [] [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 ๐] [] [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 ๐] [] [SMul ๐ E] (x : E) :
StarConvex ๐ x โ
theorem starConvex_univ {๐ : Type u_1} {E : Type u_2} [OrderedSemiring ๐] [] [SMul ๐ E] (x : E) :
StarConvex ๐ x Set.univ
theorem StarConvex.inter {๐ : Type u_1} {E : Type u_2} [OrderedSemiring ๐] [] [SMul ๐ E] {x : E} {s : Set E} {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 ๐] [] [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 ๐] [] [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 ๐] [] [SMul ๐ E] {x : E} {s : Set E} {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 ๐] [] [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 ๐] [] [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 ๐] [] [] [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 ๐] [] [Module ๐ E] {x : E} {s : Set E} (hs : StarConvex ๐ x s) (h : s.Nonempty) :
theorem starConvex_iff_forall_pos {๐ : Type u_1} {E : Type u_2} [OrderedSemiring ๐] [] [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 ๐] [] [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 ๐] [] [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 ๐] [] [Module ๐ E] (x : E) :
StarConvex ๐ x {x}
theorem StarConvex.linear_image {๐ : Type u_1} {E : Type u_2} {F : Type u_3} [OrderedSemiring ๐] [] [] [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 ๐] [] [] [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 ๐] [] [] [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 ๐] [] [] [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 ๐] [] [Module ๐ E] {x : E} {y : E} {s : Set E} {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 ๐] [] [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 ๐] [] [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 ๐] [] [Module ๐ E] {x : E} {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 ๐] [] [Module ๐ E] {x : E} {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 ๐] [] [Module ๐ E] {x : E} {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} [] [] [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} [] [] [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} [] [] [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 ๐] [] [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 ๐] [] [Module ๐ E] {x : E} {y : E} {s : Set E} (hs : StarConvex ๐ x s) (hy : x + y โ s) {t : ๐} (htโ : 0 โค t) (htโ : t โค 1) :
theorem StarConvex.smul_mem {๐ : Type u_1} {E : Type u_2} [OrderedRing ๐] [] [Module ๐ E] {x : E} {s : Set E} (hs : StarConvex ๐ 0 s) (hx : x โ s) {t : ๐} (htโ : 0 โค t) (htโ : t โค 1) :
theorem StarConvex.add_smul_sub_mem {๐ : Type u_1} {E : Type u_2} [OrderedRing ๐] [] [Module ๐ E] {x : E} {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 ๐] [] [] [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 ๐] [] [] [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 ๐] [] [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 ๐] [] [Module ๐ E] {x : E} {y : E} {s : Set E} {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 ๐] [Module ๐ E] [OrderedSMul ๐ E] {x : E} {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 ๐] [Module ๐ E] [OrderedSMul ๐ E] {x : E} {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} [] [] [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} [] [] [Module ๐ E] {x : E} {s : Set E} (hs : StarConvex ๐ 0 s) (hx : x โ s) {t : ๐} (ht : 1 โค t) :

#### Star-convex sets in an ordered space #

Relates starConvex and Set.ordConnected.

theorem Set.OrdConnected.starConvex {๐ : Type u_1} {E : Type u_2} [OrderedSemiring ๐] [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} [] {x : ๐} {s : Set ๐} (hx : x โ s) :
StarConvex ๐ x s โ s.OrdConnected
theorem StarConvex.ordConnected {๐ : Type u_1} [] {x : ๐} {s : Set ๐} (hx : x โ s) :
StarConvex ๐ x s โ s.OrdConnected

Alias of the forward direction of starConvex_iff_ordConnected.