Mathlib.Analysis.Convex.Star

StarConvex definition

 (𝕜 : Type*) {E : Type*} [Semiring 𝕜] [PartialOrder 𝕜] [AddCommMonoid E] [SMul 𝕜 E] (x : E) (s : Set E) : Prop

Full source

/-- Star-convexity of sets. `s` is star-convex at `x` if every segment from `x` to a point in `s` is
contained in `s`. -/
def StarConvex (𝕜 : Type*) {E : Type*} [Semiring 𝕜] [PartialOrder 𝕜]
    [AddCommMonoid E] [SMul 𝕜 E] (x : E) (s : Set E) : Prop :=
  ∀ ⦃y : E⦄, y ∈ s → ∀ ⦃a b : 𝕜⦄, 0 ≤ a → 0 ≤ b → a + b = 1 → a • x + b • y ∈ s

Star-convex set at a point

Informal description

A set $s$ in a vector space $E$ over a partially ordered semiring $\mathbb{K}$ is called *star-convex* at a point $x \in E$ if for every $y \in s$ and for all non-negative scalars $a, b \in \mathbb{K}$ with $a + b = 1$, the point $a \cdot x + b \cdot y$ lies in $s$. In other words, the line segment connecting $x$ to any point $y$ in $s$ is entirely contained within $s$.

starConvex_iff_segment_subset theorem

: StarConvex 𝕜 x s ↔ ∀ ⦃y⦄, y ∈ s → [x -[𝕜] y] ⊆ s

Full source

theorem starConvex_iff_segment_subset : StarConvexStarConvex 𝕜 x s ↔ ∀ ⦃y⦄, y ∈ s → [x -[𝕜] y] ⊆ s := by
  constructor
  · rintro h y hy z ⟨a, b, ha, hb, hab, rfl⟩
    exact h hy ha hb hab
  · rintro h y hy a b ha hb hab
    exact h hy ⟨a, b, ha, hb, hab, rfl⟩

Characterization of Star-Convex Sets via Segment Inclusion

Informal description

A set $s$ in a vector space $E$ over a partially ordered semiring $\mathbb{K}$ is star-convex at a point $x \in E$ if and only if for every point $y \in s$, the closed segment connecting $x$ to $y$ is entirely contained in $s$.

StarConvex.segment_subset theorem

(h : StarConvex 𝕜 x s) {y : E} (hy : y ∈ s) : [x -[𝕜] y] ⊆ s

Full source

theorem StarConvex.segment_subset (h : StarConvex 𝕜 x s) {y : E} (hy : y ∈ s) : [x -[𝕜] y][x -[𝕜] y] ⊆ s :=
  starConvex_iff_segment_subset.1 h hy

Inclusion of Segments in Star-Convex Sets

Informal description

Let $E$ be a vector space over a partially ordered semiring $\mathbb{K}$, and let $s \subseteq E$ be a set that is star-convex at a point $x \in E$. Then for any point $y \in s$, the closed segment connecting $x$ to $y$ is entirely contained in $s$.

StarConvex.openSegment_subset theorem

(h : StarConvex 𝕜 x s) {y : E} (hy : y ∈ s) : openSegment 𝕜 x y ⊆ s

Full source

theorem StarConvex.openSegment_subset (h : StarConvex 𝕜 x s) {y : E} (hy : y ∈ s) :
    openSegmentopenSegment 𝕜 x y ⊆ s :=
  (openSegment_subset_segment 𝕜 x y).trans (h.segment_subset hy)

Inclusion of Open Segments in Star-Convex Sets

Informal description

Let $E$ be a vector space over a partially ordered semiring $\mathbb{K}$, and let $s \subseteq E$ be a set that is star-convex at a point $x \in E$. Then for any point $y \in s$, the open segment connecting $x$ to $y$ is entirely contained in $s$.

starConvex_iff_pointwise_add_subset theorem

: StarConvex 𝕜 x s ↔ ∀ ⦃a b : 𝕜⦄, 0 ≤ a → 0 ≤ b → a + b = 1 → a • { x } + b • s ⊆ s

Full source

/-- Alternative definition of star-convexity, in terms of pointwise set operations. -/
theorem starConvex_iff_pointwise_add_subset :
    StarConvexStarConvex 𝕜 x s ↔ ∀ ⦃a b : 𝕜⦄, 0 ≤ a → 0 ≤ b → a + b = 1 → a • {x} + b • s ⊆ s := by
  refine
    ⟨?_, fun h y hy a b ha hb hab =>
      h ha hb hab (add_mem_add (smul_mem_smul_set <| mem_singleton _) ⟨_, hy, rfl⟩)⟩
  rintro hA a b ha hb hab w ⟨au, ⟨u, rfl : u = x, rfl⟩, bv, ⟨v, hv, rfl⟩, rfl⟩
  exact hA hv ha hb hab

Characterization of Star-Convex Sets via Minkowski Sum Inclusion

Informal description

A set $s$ in a vector space $E$ over a partially ordered semiring $\mathbb{K}$ is star-convex at a point $x \in E$ if and only if for all non-negative scalars $a, b \in \mathbb{K}$ satisfying $a + b = 1$, the Minkowski sum $a \cdot \{x\} + b \cdot s$ is contained in $s$.

starConvex_empty theorem

(x : E) : StarConvex 𝕜 x ∅

Full source

theorem starConvex_empty (x : E) : StarConvex 𝕜 x ∅ := fun _ hy => hy.elim

Empty Set is Star-Convex at Every Point

Informal description

For any point $x$ in a vector space $E$ over a partially ordered semiring $\mathbb{K}$, the empty set $\emptyset$ is star-convex at $x$.

starConvex_univ theorem

(x : E) : StarConvex 𝕜 x univ

Full source

theorem starConvex_univ (x : E) : StarConvex 𝕜 x univ := fun _ _ _ _ _ _ _ => trivial

Universal Set is Star-Convex at Every Point

Informal description

For any point $x$ in a vector space $E$ over a partially ordered semiring $\mathbb{K}$, the universal set $E$ (i.e., the set of all points in $E$) is star-convex at $x$. This means that for any $y \in E$ and any non-negative scalars $a, b \in \mathbb{K}$ with $a + b = 1$, the point $a \cdot x + b \cdot y$ lies in $E$.

StarConvex.inter theorem

(hs : StarConvex 𝕜 x s) (ht : StarConvex 𝕜 x t) : StarConvex 𝕜 x (s ∩ t)

Full source

theorem StarConvex.inter (hs : StarConvex 𝕜 x s) (ht : StarConvex 𝕜 x t) : StarConvex 𝕜 x (s ∩ t) :=
  fun _ hy _ _ ha hb hab => ⟨hs hy.left ha hb hab, ht hy.right ha hb hab⟩

Intersection of Star-Convex Sets is Star-Convex

Informal description

Let $E$ be a vector space over a partially ordered semiring $\mathbb{K}$, and let $x \in E$. If two sets $s, t \subseteq E$ are star-convex at $x$, then their intersection $s \cap t$ is also star-convex at $x$.

starConvex_sInter theorem

{S : Set (Set E)} (h : ∀ s ∈ S, StarConvex 𝕜 x s) : StarConvex 𝕜 x (⋂₀ S)

Full source

theorem starConvex_sInter {S : Set (Set E)} (h : ∀ s ∈ S, StarConvex 𝕜 x s) :
    StarConvex 𝕜 x (⋂₀ S) := fun _ hy _ _ ha hb hab s hs => h s hs (hy s hs) ha hb hab

Intersection of Star-Convex Sets is Star-Convex

Informal description

Let $E$ be a vector space over a partially ordered semiring $\mathbb{K}$, and let $x \in E$. Given a collection of sets $S$ in $E$, if every set $s \in S$ is star-convex at $x$, then the intersection $\bigcap_{s \in S} s$ is also star-convex at $x$.

starConvex_iInter theorem

{ι : Sort*} {s : ι → Set E} (h : ∀ i, StarConvex 𝕜 x (s i)) : StarConvex 𝕜 x (⋂ i, s i)

Full source

theorem starConvex_iInter {ι : Sort*} {s : ι → Set E} (h : ∀ i, StarConvex 𝕜 x (s i)) :
    StarConvex 𝕜 x (⋂ i, s i) :=
  sInter_range s ▸ starConvex_sInter <| forall_mem_range.2 h

Intersection of Star-Convex Sets is Star-Convex (Indexed Version)

Informal description

Let $E$ be a vector space over a partially ordered semiring $\mathbb{K}$, and let $x \in E$. Given an indexed family of sets $\{s_i\}_{i \in \iota}$ in $E$, if each set $s_i$ is star-convex at $x$, then the intersection $\bigcap_{i \in \iota} s_i$ is also star-convex at $x$.

starConvex_iInter₂ theorem

 {ι : Sort*} {κ : ι → Sort*} {s : (i : ι) → κ i → Set E} (h : ∀ i j, StarConvex 𝕜 x (s i j)) :
  StarConvex 𝕜 x (⋂ (i) (j), s i j)

Full source

theorem starConvex_iInter₂ {ι : Sort*} {κ : ι → Sort*} {s : (i : ι) → κ i → Set E}
    (h : ∀ i j, StarConvex 𝕜 x (s i j)) : StarConvex 𝕜 x (⋂ (i) (j), s i j) :=
  starConvex_iInter fun i => starConvex_iInter (h i)

Intersection of Doubly Indexed Star-Convex Sets is Star-Convex

Informal description

Let $\mathbb{K}$ be a partially ordered semiring and $E$ be an additive commutative monoid with a scalar multiplication by $\mathbb{K}$. Given a point $x \in E$ and a doubly indexed family of sets $\{s_{i,j}\}_{i \in \iota, j \in \kappa_i}$ in $E$ such that each $s_{i,j}$ is star-convex at $x$, then the intersection $\bigcap_{i,j} s_{i,j}$ is also star-convex at $x$.

StarConvex.union theorem

(hs : StarConvex 𝕜 x s) (ht : StarConvex 𝕜 x t) : StarConvex 𝕜 x (s ∪ t)

Full source

theorem StarConvex.union (hs : StarConvex 𝕜 x s) (ht : StarConvex 𝕜 x t) :
    StarConvex 𝕜 x (s ∪ t) := by
  rintro y (hy | hy) a b ha hb hab
  · exact Or.inl (hs hy ha hb hab)
  · exact Or.inr (ht hy ha hb hab)

Union of Star-Convex Sets is Star-Convex

Informal description

Let $\mathbb{K}$ be a partially ordered semiring and $E$ be an additive commutative monoid with a scalar multiplication by $\mathbb{K}$. Given a point $x \in E$ and two subsets $s, t \subseteq E$ that are star-convex at $x$, their union $s \cup t$ is also star-convex at $x$.

starConvex_iUnion theorem

{ι : Sort*} {s : ι → Set E} (hs : ∀ i, StarConvex 𝕜 x (s i)) : StarConvex 𝕜 x (⋃ i, s i)

Full source

theorem starConvex_iUnion {ι : Sort*} {s : ι → Set E} (hs : ∀ i, StarConvex 𝕜 x (s i)) :
    StarConvex 𝕜 x (⋃ i, s i) := by
  rintro y hy a b ha hb hab
  rw [mem_iUnion] at hy ⊢
  obtain ⟨i, hy⟩ := hy
  exact ⟨i, hs i hy ha hb hab⟩

Union of Star-Convex Sets is Star-Convex

Informal description

Let $\mathbb{K}$ be a partially ordered semiring, $E$ be an additive commutative monoid with a scalar multiplication by $\mathbb{K}$, and $x \in E$. Given an indexed family of sets $\{s_i\}_{i \in \iota}$ in $E$ such that each $s_i$ is star-convex at $x$, then the union $\bigcup_{i} s_i$ is also star-convex at $x$.

starConvex_iUnion₂ theorem

 {ι : Sort*} {κ : ι → Sort*} {s : (i : ι) → κ i → Set E} (h : ∀ i j, StarConvex 𝕜 x (s i j)) :
  StarConvex 𝕜 x (⋃ (i) (j), s i j)

Full source

theorem starConvex_iUnion₂ {ι : Sort*} {κ : ι → Sort*} {s : (i : ι) → κ i → Set E}
    (h : ∀ i j, StarConvex 𝕜 x (s i j)) : StarConvex 𝕜 x (⋃ (i) (j), s i j) :=
  starConvex_iUnion fun i => starConvex_iUnion (h i)

Star-convexity of doubly indexed unions

Informal description

Let $\mathbb{K}$ be a partially ordered semiring and $E$ be an additive commutative monoid with a scalar multiplication by $\mathbb{K}$. Given a point $x \in E$ and a doubly indexed family of sets $\{s_{i,j}\}_{i \in \iota, j \in \kappa_i}$ in $E$ such that each $s_{i,j}$ is star-convex at $x$, then the union $\bigcup_{i,j} s_{i,j}$ is also star-convex at $x$.

starConvex_sUnion theorem

{S : Set (Set E)} (hS : ∀ s ∈ S, StarConvex 𝕜 x s) : StarConvex 𝕜 x (⋃₀ S)

Full source

theorem starConvex_sUnion {S : Set (Set E)} (hS : ∀ s ∈ S, StarConvex 𝕜 x s) :
    StarConvex 𝕜 x (⋃₀ S) := by
  rw [sUnion_eq_iUnion]
  exact starConvex_iUnion fun s => hS _ s.2

Union of a Family of Star-Convex Sets is Star-Convex

Informal description

Let $\mathbb{K}$ be a partially ordered semiring, $E$ be an additive commutative monoid with a scalar multiplication by $\mathbb{K}$, and $x \in E$. Given a collection of sets $S$ in $E$ such that every set $s \in S$ is star-convex at $x$, then the union $\bigcup_{s \in S} s$ is also star-convex at $x$.

StarConvex.prod theorem

 {y : F} {s : Set E} {t : Set F} (hs : StarConvex 𝕜 x s) (ht : StarConvex 𝕜 y t) : StarConvex 𝕜 (x, y) (s ×ˢ t)

Full source

theorem StarConvex.prod {y : F} {s : Set E} {t : Set F} (hs : StarConvex 𝕜 x s)
    (ht : StarConvex 𝕜 y t) : StarConvex 𝕜 (x, y) (s ×ˢ t) := fun _ hy _ _ ha hb hab =>
  ⟨hs hy.1 ha hb hab, ht hy.2 ha hb hab⟩

Star-convexity of Cartesian Product Sets

Informal description

Let $\mathbb{K}$ be a partially ordered semiring, and let $E$ and $F$ be vector spaces over $\mathbb{K}$. Given a point $x \in E$ and a set $s \subseteq E$ that is star-convex at $x$, and a point $y \in F$ and a set $t \subseteq F$ that is star-convex at $y$, the Cartesian product set $s \times t \subseteq E \times F$ is star-convex at the point $(x, y)$.

starConvex_pi theorem

 {ι : Type*} {E : ι → Type*} [∀ 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)

Full source

theorem starConvex_pi {ι : Type*} {E : ι → Type*} [∀ 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) := fun _ hy _ _ ha hb hab i hi => ht hi (hy i hi) ha hb hab

Star-convexity of product sets

Informal description

Let $\mathbb{K}$ be a partially ordered semiring and let $\{E_i\}_{i \in \iota}$ be a family of vector spaces over $\mathbb{K}$. Given a point $x = (x_i)_{i \in \iota}$ in the product space $\prod_{i \in \iota} E_i$, a subset $s \subseteq \iota$, and a family of sets $\{t_i \subseteq E_i\}_{i \in \iota}$, if for each $i \in s$ the set $t_i$ is star-convex at $x_i$, then the product set $\prod_{i \in s} t_i$ is star-convex at $x$.

StarConvex.mem theorem

[ZeroLEOneClass 𝕜] (hs : StarConvex 𝕜 x s) (h : s.Nonempty) : x ∈ s

Full source

theorem StarConvex.mem [ZeroLEOneClass 𝕜] (hs : StarConvex 𝕜 x s) (h : s.Nonempty) : x ∈ s := by
  obtain ⟨y, hy⟩ := h
  convert hs hy zero_le_one le_rfl (add_zero 1)
  rw [one_smul, zero_smul, add_zero]

Center Point Belongs to Nonempty Star-Convex Set

Informal description

Let $\mathbb{K}$ be a partially ordered semiring where $0 \leq 1$, and let $s$ be a nonempty subset of a vector space $E$ over $\mathbb{K}$. If $s$ is star-convex at a point $x \in E$, then $x$ belongs to $s$.

starConvex_iff_forall_pos theorem

 (hx : x ∈ s) : StarConvex 𝕜 x s ↔ ∀ ⦃y⦄, y ∈ s → ∀ ⦃a b : 𝕜⦄, 0 < a → 0 < b → a + b = 1 → a • x + b • y ∈ s

Full source

theorem starConvex_iff_forall_pos (hx : x ∈ s) : StarConvexStarConvex 𝕜 x s ↔
    ∀ ⦃y⦄, y ∈ s → ∀ ⦃a b : 𝕜⦄, 0 < a → 0 < b → a + b = 1 → a • x + b • y ∈ s := by
  refine ⟨fun h y hy a b ha hb hab => h hy ha.le hb.le hab, ?_⟩
  intro h y hy a b ha hb hab
  obtain rfl | ha := ha.eq_or_lt
  · rw [zero_add] at hab
    rwa [hab, one_smul, zero_smul, zero_add]
  obtain rfl | hb := hb.eq_or_lt
  · rw [add_zero] at hab
    rwa [hab, one_smul, zero_smul, add_zero]
  exact h hy ha hb hab

Characterization of Star-Convex Sets via Positive Coefficients

Informal description

Let $s$ be a subset of a vector space $E$ over a partially ordered semiring $\mathbb{K}$, and let $x \in s$. Then $s$ is star-convex at $x$ if and only if for every $y \in s$ and for all positive scalars $a, b \in \mathbb{K}$ satisfying $a + b = 1$, the point $a \cdot x + b \cdot y$ lies in $s$.

starConvex_iff_forall_ne_pos theorem

 (hx : x ∈ s) : StarConvex 𝕜 x s ↔ ∀ ⦃y⦄, y ∈ s → x ≠ y → ∀ ⦃a b : 𝕜⦄, 0 < a → 0 < b → a + b = 1 → a • x + b • y ∈ s

Full source

theorem starConvex_iff_forall_ne_pos (hx : x ∈ s) :
    StarConvexStarConvex 𝕜 x s ↔
      ∀ ⦃y⦄, y ∈ s → x ≠ y → ∀ ⦃a b : 𝕜⦄, 0 < a → 0 < b → a + b = 1 → a • x + b • y ∈ s := by
  refine ⟨fun h y hy _ a b ha hb hab => h hy ha.le hb.le hab, ?_⟩
  intro h y hy a b ha hb hab
  obtain rfl | ha' := ha.eq_or_lt
  · rw [zero_add] at hab
    rwa [hab, zero_smul, one_smul, zero_add]
  obtain rfl | hb' := hb.eq_or_lt
  · rw [add_zero] at hab
    rwa [hab, zero_smul, one_smul, add_zero]
  obtain rfl | hxy := eq_or_ne x y
  · rwa [Convex.combo_self hab]
  exact h hy hxy ha' hb' hab

Characterization of Star-Convex Sets via Distinct Points and Positive Coefficients

Informal description

Let $s$ be a subset of a vector space $E$ over a partially ordered semiring $\mathbb{K}$, and let $x \in s$. Then $s$ is star-convex at $x$ if and only if for every $y \in s$ with $x \neq y$ and for all positive scalars $a, b \in \mathbb{K}$ satisfying $a + b = 1$, the point $a \cdot x + b \cdot y$ lies in $s$.

starConvex_iff_openSegment_subset theorem

[ZeroLEOneClass 𝕜] (hx : x ∈ s) : StarConvex 𝕜 x s ↔ ∀ ⦃y⦄, y ∈ s → openSegment 𝕜 x y ⊆ s

Full source

theorem starConvex_iff_openSegment_subset [ZeroLEOneClass 𝕜] (hx : x ∈ s) :
    StarConvexStarConvex 𝕜 x s ↔ ∀ ⦃y⦄, y ∈ s → openSegment 𝕜 x y ⊆ s :=
  starConvex_iff_segment_subset.trans <|
    forall₂_congr fun _ hy => (openSegment_subset_iff_segment_subset hx hy).symm

Characterization of Star-Convex Sets via Open Segment Inclusion

Informal description

Let $\mathbb{K}$ be a partially ordered semiring with $0 \leq 1$, and let $s$ be a subset of a $\mathbb{K}$-vector space $E$ containing a point $x$. Then $s$ is star-convex at $x$ if and only if for every $y \in s$, the open segment between $x$ and $y$ is contained in $s$.

starConvex_singleton theorem

(x : E) : StarConvex 𝕜 x { x }

Full source

theorem starConvex_singleton (x : E) : StarConvex 𝕜 x {x} := by
  rintro y (rfl : y = x) a b _ _ hab
  exact Convex.combo_self hab _

Singleton Sets are Star-Convex at Their Point

Informal description

For any vector space $E$ over a partially ordered semiring $\mathbb{K}$ and any point $x \in E$, the singleton set $\{x\}$ is star-convex at $x$.

StarConvex.linear_image theorem

(hs : StarConvex 𝕜 x s) (f : E →ₗ[𝕜] F) : StarConvex 𝕜 (f x) (f '' s)

Full source

theorem StarConvex.linear_image (hs : StarConvex 𝕜 x s) (f : E →ₗ[𝕜] F) :
    StarConvex 𝕜 (f x) (f '' s) := by
  rintro _ ⟨y, hy, rfl⟩ a b ha hb hab
  exact ⟨a • x + b • y, hs hy ha hb hab, by rw [f.map_add, f.map_smul, f.map_smul]⟩

Image of Star-Convex Set under Linear Map is Star-Convex

Informal description

Let $E$ and $F$ be vector spaces over a partially ordered semiring $\mathbb{K}$, and let $s \subseteq E$ be a star-convex set at $x \in E$. For any linear map $f : E \to F$, the image $f(s)$ is star-convex at $f(x)$ in $F$.

StarConvex.is_linear_image theorem

(hs : StarConvex 𝕜 x s) {f : E → F} (hf : IsLinearMap 𝕜 f) : StarConvex 𝕜 (f x) (f '' s)

Full source

theorem StarConvex.is_linear_image (hs : StarConvex 𝕜 x s) {f : E → F} (hf : IsLinearMap 𝕜 f) :
    StarConvex 𝕜 (f x) (f '' s) :=
  hs.linear_image <| hf.mk' f

Image of Star-Convex Set under Linear Map is Star-Convex

Informal description

Let $E$ and $F$ be vector spaces over a partially ordered semiring $\mathbb{K}$, and let $s \subseteq E$ be a star-convex set at $x \in E$. For any linear map $f : E \to F$, the image $f(s)$ is star-convex at $f(x)$ in $F$.

StarConvex.linear_preimage theorem

{s : Set F} (f : E →ₗ[𝕜] F) (hs : StarConvex 𝕜 (f x) s) : StarConvex 𝕜 x (f ⁻¹' s)

Full source

theorem StarConvex.linear_preimage {s : Set F} (f : E →ₗ[𝕜] F) (hs : StarConvex 𝕜 (f x) s) :
    StarConvex 𝕜 x (f ⁻¹' s) := by
  intro y hy a b ha hb hab
  rw [mem_preimage, f.map_add, f.map_smul, f.map_smul]
  exact hs hy ha hb hab

Preimage of Star-Convex Set under Linear Map is Star-Convex

Informal description

Let $E$ and $F$ be vector spaces over a partially ordered semiring $\mathbb{K}$, and let $s \subseteq F$ be a star-convex set at $f(x) \in F$ where $f : E \to F$ is a linear map. Then the preimage $f^{-1}(s)$ is star-convex at $x \in E$.

StarConvex.is_linear_preimage theorem

{s : Set F} {f : E → F} (hs : StarConvex 𝕜 (f x) s) (hf : IsLinearMap 𝕜 f) : StarConvex 𝕜 x (preimage f s)

Full source

theorem StarConvex.is_linear_preimage {s : Set F} {f : E → F} (hs : StarConvex 𝕜 (f x) s)
    (hf : IsLinearMap 𝕜 f) : StarConvex 𝕜 x (preimage f s) :=
  hs.linear_preimage <| hf.mk' f

Preimage of Star-Convex Set under Linear Map is Star-Convex

Informal description

Let $E$ and $F$ be vector spaces over a partially ordered semiring $\mathbb{K}$, and let $s \subseteq F$ be a star-convex set at $f(x) \in F$ for some $x \in E$. If $f : E \to F$ is a linear map, then the preimage $f^{-1}(s)$ is star-convex at $x$.

StarConvex.add theorem

{t : Set E} (hs : StarConvex 𝕜 x s) (ht : StarConvex 𝕜 y t) : StarConvex 𝕜 (x + y) (s + t)

Full source

theorem StarConvex.add {t : Set E} (hs : StarConvex 𝕜 x s) (ht : StarConvex 𝕜 y t) :
    StarConvex 𝕜 (x + y) (s + t) := by
  rw [← add_image_prod]
  exact (hs.prod ht).is_linear_image IsLinearMap.isLinearMap_add

Star-convexity of Minkowski Sum of Star-convex Sets

Informal description

Let $\mathbb{K}$ be a partially ordered semiring, and let $E$ be a vector space over $\mathbb{K}$. Given two sets $s, t \subseteq E$ that are star-convex at points $x \in s$ and $y \in t$ respectively, their Minkowski sum $s + t = \{u + v \mid u \in s, v \in t\}$ is star-convex at the point $x + y$.

StarConvex.add_left theorem

(hs : StarConvex 𝕜 x s) (z : E) : StarConvex 𝕜 (z + x) ((fun x => z + x) '' s)

Full source

theorem StarConvex.add_left (hs : StarConvex 𝕜 x s) (z : E) :
    StarConvex 𝕜 (z + x) ((fun x => z + x) '' s) := by
  intro y hy a b ha hb hab
  obtain ⟨y', hy', rfl⟩ := hy
  refine ⟨a • x + b • y', hs hy' ha hb hab, ?_⟩
  match_scalars <;> simp [hab]

Star-convexity is preserved under left translation

Informal description

Let $E$ be a vector space over a partially ordered semiring $\mathbb{K}$, and let $s \subseteq E$ be a star-convex set at $x \in E$. For any $z \in E$, the translated set $\{z + y \mid y \in s\}$ is star-convex at $z + x$.

StarConvex.add_right theorem

(hs : StarConvex 𝕜 x s) (z : E) : StarConvex 𝕜 (x + z) ((fun x => x + z) '' s)

Full source

theorem StarConvex.add_right (hs : StarConvex 𝕜 x s) (z : E) :
    StarConvex 𝕜 (x + z) ((fun x => x + z) '' s) := by
  intro y hy a b ha hb hab
  obtain ⟨y', hy', rfl⟩ := hy
  refine ⟨a • x + b • y', hs hy' ha hb hab, ?_⟩
  match_scalars <;> simp [hab]

Star-convexity is preserved under right translation

Informal description

Let $E$ be a vector space over a partially ordered semiring $\mathbb{K}$, and let $s \subseteq E$ be a star-convex set at $x \in E$. For any $z \in E$, the translated set $\{y + z \mid y \in s\}$ is star-convex at $x + z$.

StarConvex.preimage_add_right theorem

(hs : StarConvex 𝕜 (z + x) s) : StarConvex 𝕜 x ((fun x => z + x) ⁻¹' s)

Full source

/-- The translation of a star-convex set is also star-convex. -/
theorem StarConvex.preimage_add_right (hs : StarConvex 𝕜 (z + x) s) :
    StarConvex 𝕜 x ((fun x => z + x) ⁻¹' s) := by
  intro y hy a b ha hb hab
  have h := hs hy ha hb hab
  rwa [smul_add, smul_add, add_add_add_comm, ← add_smul, hab, one_smul] at h

Preimage of Star-Convex Set under Right Translation is Star-Convex

Informal description

Let $E$ be a vector space over a partially ordered semiring $\mathbb{K}$, and let $s$ be a subset of $E$. If $s$ is star-convex at the point $z + x$, then the preimage of $s$ under the function $y \mapsto z + y$ is star-convex at $x$.

StarConvex.preimage_add_left theorem

(hs : StarConvex 𝕜 (x + z) s) : StarConvex 𝕜 x ((fun x => x + z) ⁻¹' s)

Full source

/-- The translation of a star-convex set is also star-convex. -/
theorem StarConvex.preimage_add_left (hs : StarConvex 𝕜 (x + z) s) :
    StarConvex 𝕜 x ((fun x => x + z) ⁻¹' s) := by
  rw [add_comm] at hs
  simpa only [add_comm] using hs.preimage_add_right

Preimage of Star-Convex Set under Left Translation is Star-Convex

Informal description

Let $E$ be a vector space over a partially ordered semiring $\mathbb{K}$, and let $s$ be a subset of $E$. If $s$ is star-convex at the point $x + z$, then the preimage of $s$ under the function $y \mapsto y + z$ is star-convex at $x$.

StarConvex.sub' theorem

{s : Set (E × E)} (hs : StarConvex 𝕜 (x, y) s) : StarConvex 𝕜 (x - y) ((fun x : E × E => x.1 - x.2) '' s)

Full source

theorem StarConvex.sub' {s : Set (E × E)} (hs : StarConvex 𝕜 (x, y) s) :
    StarConvex 𝕜 (x - y) ((fun x : E × E => x.1 - x.2) '' s) :=
  hs.is_linear_image IsLinearMap.isLinearMap_sub

Star-convexity of the difference set under subtraction

Informal description

Let $E$ be a vector space over a partially ordered semiring $\mathbb{K}$, and let $s \subseteq E \times E$ be a star-convex set at $(x, y) \in E \times E$. Then the image of $s$ under the subtraction map $(u,v) \mapsto u - v$ is star-convex at $x - y \in E$.

StarConvex.smul theorem

(hs : StarConvex 𝕜 x s) (c : 𝕜) : StarConvex 𝕜 (c • x) (c • s)

Full source

theorem StarConvex.smul (hs : StarConvex 𝕜 x s) (c : 𝕜) : StarConvex 𝕜 (c • x) (c • s) :=
  hs.linear_image <| LinearMap.lsmul _ _ c

Scalar Multiplication Preserves Star-Convexity

Informal description

Let $E$ be a vector space over a partially ordered semiring $\mathbb{K}$, and let $s \subseteq E$ be a star-convex set at $x \in E$. Then for any scalar $c \in \mathbb{K}$, the scaled set $c \cdot s$ is star-convex at the scaled point $c \cdot x$.

StarConvex.zero_smul theorem

(hs : StarConvex 𝕜 0 s) (c : 𝕜) : StarConvex 𝕜 0 (c • s)

Full source

theorem StarConvex.zero_smul (hs : StarConvex 𝕜 0 s) (c : 𝕜) : StarConvex 𝕜 0 (c • s) := by
  simpa using hs.smul c

Star-convexity at zero is preserved under scalar multiplication

Informal description

Let $E$ be a vector space over a partially ordered semiring $\mathbb{K}$, and let $s \subseteq E$ be a star-convex set at $0 \in E$. Then for any scalar $c \in \mathbb{K}$, the scaled set $c \cdot s$ is star-convex at $0 \in E$.

StarConvex.preimage_smul theorem

{c : 𝕜} (hs : StarConvex 𝕜 (c • x) s) : StarConvex 𝕜 x ((fun z => c • z) ⁻¹' s)

Full source

theorem StarConvex.preimage_smul {c : 𝕜} (hs : StarConvex 𝕜 (c • x) s) :
    StarConvex 𝕜 x ((fun z => c • z) ⁻¹' s) :=
  hs.linear_preimage (LinearMap.lsmul _ _ c)

Star-convexity of the preimage under scaling

Informal description

Let $\mathbb{K}$ be a partially ordered semiring, $E$ be a vector space over $\mathbb{K}$, and $s$ be a subset of $E$. For any scalar $c \in \mathbb{K}$ and any point $x \in E$, if $s$ is star-convex at $c \cdot x$, then the preimage of $s$ under the scaling map $z \mapsto c \cdot z$ is star-convex at $x$.

StarConvex.affinity theorem

(hs : StarConvex 𝕜 x s) (z : E) (c : 𝕜) : StarConvex 𝕜 (z + c • x) ((fun x => z + c • x) '' s)

Full source

theorem StarConvex.affinity (hs : StarConvex 𝕜 x s) (z : E) (c : 𝕜) :
    StarConvex 𝕜 (z + c • x) ((fun x => z + c • x) '' s) := by
  have h := (hs.smul c).add_left z
  rwa [← image_smul, image_image] at h

Star-convexity is preserved under affine transformations

Informal description

Let $E$ be a vector space over a partially ordered semiring $\mathbb{K}$, and let $s \subseteq E$ be a star-convex set at $x \in E$. For any $z \in E$ and any scalar $c \in \mathbb{K}$, the affine image $\{z + c \cdot y \mid y \in s\}$ is star-convex at $z + c \cdot x$.

starConvex_zero_iff theorem

: StarConvex 𝕜 0 s ↔ ∀ ⦃x : E⦄, x ∈ s → ∀ ⦃a : 𝕜⦄, 0 ≤ a → a ≤ 1 → a • x ∈ s

Full source

theorem starConvex_zero_iff :
    StarConvexStarConvex 𝕜 0 s ↔ ∀ ⦃x : E⦄, x ∈ s → ∀ ⦃a : 𝕜⦄, 0 ≤ a → a ≤ 1 → a • x ∈ s := by
  refine
    forall_congr' fun x => forall_congr' fun _ => ⟨fun h a ha₀ ha₁ => ?_, fun h a b ha hb hab => ?_⟩
  · simpa only [sub_add_cancel, eq_self_iff_true, forall_true_left, zero_add, smul_zero] using
      h (sub_nonneg_of_le ha₁) ha₀
  · rw [smul_zero, zero_add]
    exact h hb (by rw [← hab]; exact le_add_of_nonneg_left ha)

Characterization of Star-Convex Sets at Origin: $s$ is star-convex at $0$ iff closed under scaling by $[0,1]$

Informal description

A set $s$ in a vector space $E$ over a partially ordered semiring $\mathbb{K}$ is star-convex at the origin $0$ if and only if for every $x \in s$ and every scalar $a \in \mathbb{K}$ with $0 \leq a \leq 1$, the scaled point $a \cdot x$ belongs to $s$.

StarConvex.add_smul_mem theorem

(hs : StarConvex 𝕜 x s) (hy : x + y ∈ s) {t : 𝕜} (ht₀ : 0 ≤ t) (ht₁ : t ≤ 1) : x + t • y ∈ s

Full source

theorem StarConvex.add_smul_mem (hs : StarConvex 𝕜 x s) (hy : x + y ∈ s) {t : 𝕜} (ht₀ : 0 ≤ t)
    (ht₁ : t ≤ 1) : x + t • y ∈ s := by
  have h : x + t • y = (1 - t) • x + t • (x + y) := by
    rw [smul_add, ← add_assoc, ← add_smul, sub_add_cancel, one_smul]
  rw [h]
  exact hs hy (sub_nonneg_of_le ht₁) ht₀ (sub_add_cancel _ _)

Star-convexity implies closedness under linear interpolation from center point

Informal description

Let $E$ be a vector space over a partially ordered semiring $\mathbb{K}$, and let $s \subseteq E$ be a star-convex set at $x \in E$. If $x + y \in s$ for some $y \in E$, then for any scalar $t \in \mathbb{K}$ with $0 \leq t \leq 1$, the point $x + t \cdot y$ also lies in $s$.

StarConvex.smul_mem theorem

(hs : StarConvex 𝕜 0 s) (hx : x ∈ s) {t : 𝕜} (ht₀ : 0 ≤ t) (ht₁ : t ≤ 1) : t • x ∈ s

Full source

theorem StarConvex.smul_mem (hs : StarConvex 𝕜 0 s) (hx : x ∈ s) {t : 𝕜} (ht₀ : 0 ≤ t)
    (ht₁ : t ≤ 1) : t • x ∈ s := by simpa using hs.add_smul_mem (by simpa using hx) ht₀ ht₁

Star-convexity at origin implies closedness under scaling by $[0,1]$

Informal description

Let $E$ be a vector space over a partially ordered semiring $\mathbb{K}$, and let $s \subseteq E$ be a star-convex set at $0 \in E$. For any $x \in s$ and any scalar $t \in \mathbb{K}$ with $0 \leq t \leq 1$, the scaled point $t \cdot x$ lies in $s$.

StarConvex.add_smul_sub_mem theorem

(hs : StarConvex 𝕜 x s) (hy : y ∈ s) {t : 𝕜} (ht₀ : 0 ≤ t) (ht₁ : t ≤ 1) : x + t • (y - x) ∈ s

Full source

theorem StarConvex.add_smul_sub_mem (hs : StarConvex 𝕜 x s) (hy : y ∈ s) {t : 𝕜} (ht₀ : 0 ≤ t)
    (ht₁ : t ≤ 1) : x + t • (y - x) ∈ s := by
  apply hs.segment_subset hy
  rw [segment_eq_image']
  exact mem_image_of_mem _ ⟨ht₀, ht₁⟩

Star-convexity implies closedness under linear interpolation

Informal description

Let $E$ be a vector space over a partially ordered semiring $\mathbb{K}$, and let $s \subseteq E$ be a star-convex set at $x \in E$. For any point $y \in s$ and any scalar $t \in \mathbb{K}$ with $0 \leq t \leq 1$, the point $x + t(y - x)$ lies in $s$.

StarConvex.affine_preimage theorem

(f : E →ᵃ[𝕜] F) {s : Set F} (hs : StarConvex 𝕜 (f x) s) : StarConvex 𝕜 x (f ⁻¹' s)

Full source

/-- The preimage of a star-convex set under an affine map is star-convex. -/
theorem StarConvex.affine_preimage (f : E →ᵃ[𝕜] F) {s : Set F} (hs : StarConvex 𝕜 (f x) s) :
    StarConvex 𝕜 x (f ⁻¹' s) := by
  intro y hy a b ha hb hab
  rw [mem_preimage, Convex.combo_affine_apply hab]
  exact hs hy ha hb hab

Preimage of a Star-Convex Set under an Affine Map is Star-Convex

Informal description

Let $E$ and $F$ be vector spaces over a partially ordered semiring $\mathbb{K}$, and let $f : E \to F$ be an affine map. If a set $s \subseteq F$ is star-convex at the point $f(x) \in F$, then the preimage $f^{-1}(s) \subseteq E$ is star-convex at $x \in E$.

StarConvex.affine_image theorem

(f : E →ᵃ[𝕜] F) {s : Set E} (hs : StarConvex 𝕜 x s) : StarConvex 𝕜 (f x) (f '' s)

Full source

/-- The image of a star-convex set under an affine map is star-convex. -/
theorem StarConvex.affine_image (f : E →ᵃ[𝕜] F) {s : Set E} (hs : StarConvex 𝕜 x s) :
    StarConvex 𝕜 (f x) (f '' s) := by
  rintro y ⟨y', ⟨hy', hy'f⟩⟩ a b ha hb hab
  refine ⟨a • x + b • y', ⟨hs hy' ha hb hab, ?_⟩⟩
  rw [Convex.combo_affine_apply hab, hy'f]

Image of a Star-Convex Set under an Affine Map is Star-Convex

Informal description

Let $E$ and $F$ be vector spaces over a partially ordered semiring $\mathbb{K}$, and let $f : E \to F$ be an affine map. If a set $s \subseteq E$ is star-convex at a point $x \in E$, then the image $f(s)$ is star-convex at $f(x)$ in $F$.

StarConvex.neg theorem

(hs : StarConvex 𝕜 x s) : StarConvex 𝕜 (-x) (-s)

Full source

theorem StarConvex.neg (hs : StarConvex 𝕜 x s) : StarConvex 𝕜 (-x) (-s) := by
  rw [← image_neg_eq_neg]
  exact hs.is_linear_image IsLinearMap.isLinearMap_neg

Negation Preserves Star-Convexity

Informal description

Let $E$ be a vector space over a partially ordered semiring $\mathbb{K}$, and let $s \subseteq E$ be a star-convex set at $x \in E$. Then the negation $-s = \{-y \mid y \in s\}$ is star-convex at $-x$.

StarConvex.sub theorem

(hs : StarConvex 𝕜 x s) (ht : StarConvex 𝕜 y t) : StarConvex 𝕜 (x - y) (s - t)

Full source

theorem StarConvex.sub (hs : StarConvex 𝕜 x s) (ht : StarConvex 𝕜 y t) :
    StarConvex 𝕜 (x - y) (s - t) := by
  simp_rw [sub_eq_add_neg]
  exact hs.add ht.neg

Star-convexity of Minkowski Difference of Star-convex Sets

Informal description

Let $\mathbb{K}$ be a partially ordered semiring and $E$ be a vector space over $\mathbb{K}$. Given two sets $s, t \subseteq E$ that are star-convex at points $x \in s$ and $y \in t$ respectively, their Minkowski difference $s - t = \{u - v \mid u \in s, v \in t\}$ is star-convex at the point $x - y$.

starConvex_compl_Iic theorem

(h : x < y) : StarConvex 𝕜 y (Iic x)ᶜ

Full source

/-- If `x < y`, then `(Set.Iic x)ᶜ` is star convex at `y`. -/
lemma starConvex_compl_Iic (h : x < y) : StarConvex 𝕜 y (Iic x)ᶜ := by
  refine (starConvex_iff_forall_pos <| by simp [h.not_le]).mpr fun z hz a b ha hb hab ↦ ?_
  rw [mem_compl_iff, mem_Iic] at hz ⊢
  contrapose! hz
  refine (lt_of_smul_lt_smul_of_nonneg_left ?_ hb.le).le
  calc
    b • z ≤ (a + b) • x - a • y := by rwa [le_sub_iff_add_le', hab, one_smul]
    _ < b • x := by
      rw [add_smul, sub_lt_iff_lt_add']
      gcongr

Star-convexity of the complement of $(-\infty, x]$ at $y$ when $x < y$

Informal description

Let $\mathbb{K}$ be a partially ordered semiring and $E$ be an ordered additive commutative monoid with a scalar multiplication operation. For any elements $x, y \in E$ such that $x < y$, the complement of the left-infinite right-closed interval $(-\infty, x]$ is star-convex at $y$. That is, the set $(Iic x)^c = \{ z \in E \mid z > x \}$ is star-convex at $y$.

starConvex_compl_Ici theorem

(h : x < y) : StarConvex 𝕜 x (Ici y)ᶜ

Full source

/-- If `x < y`, then `(Set.Ici y)ᶜ` is star convex at `x`. -/
lemma starConvex_compl_Ici (h : x < y) : StarConvex 𝕜 x (Ici y)ᶜ :=
  starConvex_compl_Iic (E := Eᵒᵈ) h

Star-convexity of the complement of $[y, \infty)$ at $x$ when $x < y$

Informal description

Let $\mathbb{K}$ be a partially ordered semiring and $E$ be an ordered additive commutative monoid with a scalar multiplication operation. For any elements $x, y \in E$ such that $x < y$, the complement of the right-closed left-infinite interval $[y, \infty)$ is star-convex at $x$. That is, the set $(Ici y)^c = \{ z \in E \mid z < y \}$ is star-convex at $x$.

starConvex_iff_div theorem

 : StarConvex 𝕜 x s ↔ ∀ ⦃y⦄, y ∈ s → ∀ ⦃a b : 𝕜⦄, 0 ≤ a → 0 ≤ b → 0 < a + b → (a / (a + b)) • x + (b / (a + b)) • y ∈ s

Full source

/-- Alternative definition of star-convexity, using division. -/
theorem starConvex_iff_div : StarConvexStarConvex 𝕜 x s ↔ ∀ ⦃y⦄, y ∈ s →
    ∀ ⦃a b : 𝕜⦄, 0 ≤ a → 0 ≤ b → 0 < a + b → (a / (a + b)) • x + (b / (a + b)) • y ∈ s :=
  ⟨fun h y hy a b ha hb hab => by
    apply h hy
    · positivity
    · positivity
    · rw [← add_div]
      exact div_self hab.ne',
  fun h y hy a b ha hb hab => by
    have h' := h hy ha hb
    rw [hab, div_one, div_one] at h'
    exact h' zero_lt_one⟩

Star-Convexity via Division: $\text{StarConvex}(\mathbb{K}, x, s) \iff \forall y \in s, \forall a,b \geq 0, a+b>0 \Rightarrow \frac{a}{a+b}x + \frac{b}{a+b}y \in s$

Informal description

A set $s$ in a vector space $E$ over a partially ordered semiring $\mathbb{K}$ is star-convex at a point $x \in E$ if and only if for every $y \in s$ and for all non-negative scalars $a, b \in \mathbb{K}$ with $a + b > 0$, the point $\left(\frac{a}{a+b}\right) \cdot x + \left(\frac{b}{a+b}\right) \cdot y$ lies in $s$.

StarConvex.mem_smul theorem

(hs : StarConvex 𝕜 0 s) (hx : x ∈ s) {t : 𝕜} (ht : 1 ≤ t) : x ∈ t • s

Full source

theorem StarConvex.mem_smul (hs : StarConvex 𝕜 0 s) (hx : x ∈ s) {t : 𝕜} (ht : 1 ≤ t) :
    x ∈ t • s := by
  rw [mem_smul_set_iff_inv_smul_mem₀ (zero_lt_one.trans_le ht).ne']
  exact hs.smul_mem hx (by positivity) (inv_le_one_of_one_le₀ ht)

Star-convexity at origin implies $x \in t \cdot s$ for $t \geq 1$

Informal description

Let $E$ be a vector space over a partially ordered semiring $\mathbb{K}$, and let $s \subseteq E$ be a star-convex set at $0 \in E$. For any $x \in s$ and any scalar $t \in \mathbb{K}$ with $t \geq 1$, the point $x$ lies in the scaled set $t \cdot s$.

Set.OrdConnected.starConvex theorem

 [Semiring 𝕜] [PartialOrder 𝕜] [AddCommMonoid E] [PartialOrder E] [IsOrderedAddMonoid 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

Full source

/-- 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 Set.OrdConnected.starConvex [Semiring 𝕜] [PartialOrder 𝕜]
    [AddCommMonoid E] [PartialOrder E] [IsOrderedAddMonoid 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 := by
  intro y hy a b ha hb hab
  obtain hxy | hyx := h _ hy
  · refine hs.out hx hy (mem_Icc.2 ⟨?_, ?_⟩)
    · calc
        x = a • x + b • x := (Convex.combo_self hab _).symm
        _ ≤ a • x + b • y := by gcongr
    calc
      a • x + b • y ≤ a • y + b • y := by gcongr
      _ = y := Convex.combo_self hab _
  · refine hs.out hy hx (mem_Icc.2 ⟨?_, ?_⟩)
    · calc
        y = a • y + b • y := (Convex.combo_self hab _).symm
        _ ≤ a • x + b • y := by gcongr
    calc
      a • x + b • y ≤ a • x + b • x := by gcongr
      _ = x := Convex.combo_self hab _

Order-Connected Sets with Comparable Elements are Star-Convex

Informal description

Let $\mathbb{K}$ be a partially ordered semiring and $E$ be a partially ordered additive commutative monoid with a scalar multiplication by $\mathbb{K}$ that is compatible with the orders. For a set $s \subseteq E$ that is order-connected, if $x \in s$ and every element $y \in s$ is comparable with $x$ (i.e., $x \leq y$ or $y \leq x$), then $s$ is star-convex at $x$.

starConvex_iff_ordConnected theorem

 [Field 𝕜] [LinearOrder 𝕜] [IsStrictOrderedRing 𝕜] {x : 𝕜} {s : Set 𝕜} (hx : x ∈ s) : StarConvex 𝕜 x s ↔ s.OrdConnected

Full source

theorem starConvex_iff_ordConnected [Field 𝕜] [LinearOrder 𝕜] [IsStrictOrderedRing 𝕜]
    {x : 𝕜} {s : Set 𝕜} (hx : x ∈ s) :
    StarConvexStarConvex 𝕜 x s ↔ s.OrdConnected := by
  simp_rw [ordConnected_iff_uIcc_subset_left hx, starConvex_iff_segment_subset, segment_eq_uIcc]

Star-convexity at a point is equivalent to order-connectedness in a linearly ordered field

Informal description

Let $\mathbb{K}$ be a linearly ordered field with a strict ordered ring structure, $x \in \mathbb{K}$, and $s \subseteq \mathbb{K}$ a set containing $x$. Then $s$ is star-convex at $x$ if and only if $s$ is order-connected. Here, a set $s$ is *star-convex* at $x$ if for every $y \in s$, the closed segment joining $x$ and $y$ is contained in $s$. A set $s$ is *order-connected* if for any two points $y, z \in s$, the closed interval $[\min(y, z), \max(y, z)]$ is contained in $s$.

Mathlib.Analysis.Convex.Star

Main declarations

Implementation notes

TODO