Star-convex sets #
This file defines star-convex sets in a convex space.
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.
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.
def
Convexity.IsStarConvexSet
(R : Type u_1)
{X : Type u_2}
[Semiring R]
[PartialOrder R]
[IsStrictOrderedRing R]
[ConvexSpace R X]
(x : X)
(s : Set X)
:
A set s is star-convex at a point x if every segment from x to a point in s is
contained in s.
TODO: Replace StarConvex with this predicate.
Equations
- Convexity.IsStarConvexSet R x s = ∀ ⦃y : X⦄, y ∈ s → ∀ ⦃a b : R⦄ (ha : 0 ≤ a) (hb : 0 ≤ b) (hab : a + b = 1), Convexity.convexCombPair a b ha hb hab x y ∈ s
Instances For
@[simp]
theorem
Convexity.IsStarConvexSet.empty
{R : Type u_1}
{X : Type u_2}
[Semiring R]
[PartialOrder R]
[IsStrictOrderedRing R]
[ConvexSpace R X]
{x : X}
:
IsStarConvexSet R x ∅
@[simp]
theorem
Convexity.IsStarConvexSet.univ
{R : Type u_1}
{X : Type u_2}
[Semiring R]
[PartialOrder R]
[IsStrictOrderedRing R]
[ConvexSpace R X]
{x : X}
:
@[simp]
theorem
Convexity.IsStarConvexSet.singleton
{R : Type u_1}
{X : Type u_2}
[Semiring R]
[PartialOrder R]
[IsStrictOrderedRing R]
[ConvexSpace R X]
{x : X}
:
IsStarConvexSet R x {x}
theorem
Convexity.IsStarConvexSet.inter
{R : Type u_1}
{X : Type u_2}
[Semiring R]
[PartialOrder R]
[IsStrictOrderedRing R]
[ConvexSpace R X]
{x : X}
{s t : Set X}
(hs : IsStarConvexSet R x s)
(ht : IsStarConvexSet R x t)
:
IsStarConvexSet R x (s ∩ t)
theorem
Convexity.IsStarConvexSet.union
{R : Type u_1}
{X : Type u_2}
[Semiring R]
[PartialOrder R]
[IsStrictOrderedRing R]
[ConvexSpace R X]
{x : X}
{s t : Set X}
(hs : IsStarConvexSet R x s)
(ht : IsStarConvexSet R x t)
:
IsStarConvexSet R x (s ∪ t)
theorem
Convexity.IsStarConvexSet.sInter
{R : Type u_1}
{X : Type u_2}
[Semiring R]
[PartialOrder R]
[IsStrictOrderedRing R]
[ConvexSpace R X]
{x : X}
{S : Set (Set X)}
(hS : ∀ s ∈ S, IsStarConvexSet R x s)
:
IsStarConvexSet R x (⋂₀ S)
theorem
Convexity.IsStarConvexSet.iInter
{R : Type u_1}
{X : Type u_2}
{ι : Sort u_4}
[Semiring R]
[PartialOrder R]
[IsStrictOrderedRing R]
[ConvexSpace R X]
{x : X}
{s : ι → Set X}
(hs : ∀ (i : ι), IsStarConvexSet R x (s i))
:
IsStarConvexSet R x (⋂ (i : ι), s i)
theorem
Convexity.IsStarConvexSet.iInter₂
{R : Type u_1}
{X : Type u_2}
{ι : Sort u_4}
{κ : ι → Sort u_5}
[Semiring R]
[PartialOrder R]
[IsStrictOrderedRing R]
[ConvexSpace R X]
{x : X}
{s : (i : ι) → κ i → Set X}
(h : ∀ (i : ι) (j : κ i), IsStarConvexSet R x (s i j))
:
IsStarConvexSet R x (⋂ (i : ι), ⋂ (j : κ i), s i j)
theorem
Convexity.IsStarConvexSet.sUnion
{R : Type u_1}
{X : Type u_2}
[Semiring R]
[PartialOrder R]
[IsStrictOrderedRing R]
[ConvexSpace R X]
{x : X}
{S : Set (Set X)}
(hS : ∀ s ∈ S, IsStarConvexSet R x s)
:
IsStarConvexSet R x (⋃₀ S)
theorem
Convexity.IsStarConvexSet.iUnion
{R : Type u_1}
{X : Type u_2}
{ι : Sort u_4}
[Semiring R]
[PartialOrder R]
[IsStrictOrderedRing R]
[ConvexSpace R X]
{x : X}
{s : ι → Set X}
(hs : ∀ (i : ι), IsStarConvexSet R x (s i))
:
IsStarConvexSet R x (⋃ (i : ι), s i)
theorem
Convexity.IsStarConvexSet.iUnion₂
{R : Type u_1}
{X : Type u_2}
{ι : Sort u_4}
{κ : ι → Sort u_5}
[Semiring R]
[PartialOrder R]
[IsStrictOrderedRing R]
[ConvexSpace R X]
{x : X}
{s : (i : ι) → κ i → Set X}
(h : ∀ (i : ι) (j : κ i), IsStarConvexSet R x (s i j))
:
IsStarConvexSet R x (⋃ (i : ι), ⋃ (j : κ i), s i j)
theorem
Convexity.IsConvexSet.isStarConvexSet
{R : Type u_1}
{X : Type u_2}
[Semiring R]
[PartialOrder R]
[IsStrictOrderedRing R]
[ConvexSpace R X]
{x : X}
{s : Set X}
(hs : IsConvexSet R s)
(hx : x ∈ s)
:
IsStarConvexSet R x s
theorem
Convexity.IsStarConvexSet.mem
{R : Type u_1}
{X : Type u_2}
[Semiring R]
[PartialOrder R]
[IsStrictOrderedRing R]
[ConvexSpace R X]
{x : X}
{s : Set X}
(hs : IsStarConvexSet R x s)
(hs₀ : s.Nonempty)
:
theorem
Convexity.IsStarConvexSet.preimage
{R : Type u_1}
{X : Type u_2}
{Y : Type u_3}
[Semiring R]
[PartialOrder R]
[IsStrictOrderedRing R]
[ConvexSpace R X]
[ConvexSpace R Y]
{f : X → Y}
{x : X}
{s : Set Y}
(hf : IsAffineMap R f)
(hs : IsStarConvexSet R (f x) s)
:
IsStarConvexSet R x (f ⁻¹' s)
theorem
Convexity.IsStarConvexSet.image
{R : Type u_1}
{X : Type u_2}
{Y : Type u_3}
[Semiring R]
[PartialOrder R]
[IsStrictOrderedRing R]
[ConvexSpace R X]
[ConvexSpace R Y]
{f : X → Y}
{x : X}
{s : Set X}
(hf : IsAffineMap R f)
(hs : IsStarConvexSet R x s)
:
IsStarConvexSet R (f x) (f '' s)
theorem
Convexity.IsStarConvexSet.prod
{R : Type u_1}
{X : Type u_2}
{Y : Type u_3}
[Semiring R]
[PartialOrder R]
[IsStrictOrderedRing R]
[ConvexSpace R X]
[ConvexSpace R Y]
{x : X}
{s : Set X}
{t : Set Y}
{y : Y}
(hs : IsStarConvexSet R x s)
(ht : IsStarConvexSet R y t)
:
IsStarConvexSet R (x, y) (s ×ˢ t)
theorem
Convexity.IsStarConvexSet.pi
{R : Type u_1}
[Semiring R]
[PartialOrder R]
[IsStrictOrderedRing R]
{ι : Type u_6}
{X : ι → Type u_7}
[(i : ι) → ConvexSpace R (X i)]
{s : Set ι}
{x : (i : ι) → X i}
{t : (i : ι) → Set (X i)}
(ht : ∀ i ∈ s, IsStarConvexSet R (x i) (t i))
:
IsStarConvexSet R x (s.pi t)