Convex hull

This file defines the convex hull of a set in a convex space. convexHull R s is the smallest convex set containing s. In order theory speak, this is a closure operator.

def Convexity.convexHull (R : Type u_1) {X : Type u_2} [Semiring R] [PartialOrder R] [IsStrictOrderedRing R] [ConvexSpace R X] : ClosureOperator (Set X)

The convex hull of a set s is the minimal convex set that includes s.

Equations

• Convexity.convexHull R = ClosureOperator.ofCompletePred (Convexity.IsConvexSet R) ⋯

theorem Convexity.subset_convexHull_iff {R : Type u_1} {X : Type u_2} [Semiring R] [PartialOrder R] [IsStrictOrderedRing R] [ConvexSpace R X] {s t : Set X} : t ⊆ (convexHull R) s ↔ ∀ (C : Set X), s ⊆ C → IsConvexSet R C → t ⊆ C

@[simp]

theorem Convexity.subset_convexHull_self {R : Type u_1} {X : Type u_2} [Semiring R] [PartialOrder R] [IsStrictOrderedRing R] [ConvexSpace R X] {s : Set X} : s ⊆ (convexHull R) s

theorem Convexity.IsConvexSet.convexHull {R : Type u_1} {X : Type u_2} [Semiring R] [PartialOrder R] [IsStrictOrderedRing R] [ConvexSpace R X] {s : Set X} : IsConvexSet R ((convexHull R) s)

theorem Convexity.convexHull_eq_iInter {R : Type u_1} {X : Type u_2} [Semiring R] [PartialOrder R] [IsStrictOrderedRing R] [ConvexSpace R X] {s : Set X} : (convexHull R) s = ⋂ (t : Set X), ⋂ (_ : s ⊆ t), ⋂ (_ : IsConvexSet R t), t

theorem Convexity.mem_convexHull_iff {R : Type u_1} {X : Type u_2} [Semiring R] [PartialOrder R] [IsStrictOrderedRing R] [ConvexSpace R X] {s : Set X} {x : X} : x ∈ (convexHull R) s ↔ ∀ (t : Set X), s ⊆ t → IsConvexSet R t → x ∈ t

theorem Convexity.convexHull_min {R : Type u_1} {X : Type u_2} [Semiring R] [PartialOrder R] [IsStrictOrderedRing R] [ConvexSpace R X] {C s : Set X} : s ⊆ C → IsConvexSet R C → (convexHull R) s ⊆ C

theorem Convexity.IsConvexSet.convexHull_subset_iff {R : Type u_1} {X : Type u_2} [Semiring R] [PartialOrder R] [IsStrictOrderedRing R] [ConvexSpace R X] {C s : Set X} (hC : IsConvexSet R C) : (convexHull R) s ⊆ C ↔ s ⊆ C

theorem Convexity.convexHull_mono {R : Type u_1} {X : Type u_2} [Semiring R] [PartialOrder R] [IsStrictOrderedRing R] [ConvexSpace R X] {s t : Set X} (hst : s ⊆ t) : (convexHull R) s ⊆ (convexHull R) t

theorem Convexity.convexHull_eq_self {R : Type u_1} {X : Type u_2} [Semiring R] [PartialOrder R] [IsStrictOrderedRing R] [ConvexSpace R X] {C : Set X} : (convexHull R) C = C ↔ IsConvexSet R C

theorem Convexity.convexHull_subset_self {R : Type u_1} {X : Type u_2} [Semiring R] [PartialOrder R] [IsStrictOrderedRing R] [ConvexSpace R X] {C : Set X} : (convexHull R) C ⊆ C ↔ IsConvexSet R C

theorem Convexity.IsConvexSet.convexHull_eq_self {R : Type u_1} {X : Type u_2} [Semiring R] [PartialOrder R] [IsStrictOrderedRing R] [ConvexSpace R X] {C : Set X} : IsConvexSet R C → (convexHull R) C = C

Alias of the reverse direction of Convexity.convexHull_eq_self.

@[simp]

theorem Convexity.convexHull_empty (R : Type u_1) {X : Type u_2} [Semiring R] [PartialOrder R] [IsStrictOrderedRing R] [ConvexSpace R X] : (convexHull R) ∅ = ∅

@[simp]

theorem Convexity.convexHull_eq_empty {R : Type u_1} {X : Type u_2} [Semiring R] [PartialOrder R] [IsStrictOrderedRing R] [ConvexSpace R X] {s : Set X} : (convexHull R) s = ∅ ↔ s = ∅

@[simp]

theorem Convexity.convexHull_nonempty {R : Type u_1} {X : Type u_2} [Semiring R] [PartialOrder R] [IsStrictOrderedRing R] [ConvexSpace R X] {s : Set X} : ((convexHull R) s).Nonempty ↔ s.Nonempty

theorem Convexity.Set.Nonempty.convexHull' {R : Type u_1} {X : Type u_2} [Semiring R] [PartialOrder R] [IsStrictOrderedRing R] [ConvexSpace R X] {s : Set X} : s.Nonempty → ((convexHull R) s).Nonempty

Alias of the reverse direction of Convexity.convexHull_nonempty.

@[simp]

theorem Convexity.convexHull_singleton (R : Type u_1) {X : Type u_2} [Semiring R] [PartialOrder R] [IsStrictOrderedRing R] [ConvexSpace R X] (x : X) : (convexHull R) {x} = {x}

@[simp]

theorem Convexity.convexHull_univ {R : Type u_1} {X : Type u_2} [Semiring R] [PartialOrder R] [IsStrictOrderedRing R] [ConvexSpace R X] : (convexHull R) Set.univ = Set.univ

@[simp]

theorem Convexity.convexHull_eq_singleton {R : Type u_1} {X : Type u_2} [Semiring R] [PartialOrder R] [IsStrictOrderedRing R] [ConvexSpace R X] {s : Set X} {x : X} : (convexHull R) s = {x} ↔ s = {x}

@[simp]

theorem Convexity.convexHull_convexHull_union (R : Type u_1) {X : Type u_2} [Semiring R] [PartialOrder R] [IsStrictOrderedRing R] [ConvexSpace R X] (s t : Set X) : (convexHull R) ((convexHull R) s ∪ t) = (convexHull R) (s ∪ t)

@[simp]

theorem Convexity.convexHull_union_convexHull (R : Type u_1) {X : Type u_2} [Semiring R] [PartialOrder R] [IsStrictOrderedRing R] [ConvexSpace R X] (s t : Set X) : (convexHull R) (s ∪ (convexHull R) t) = (convexHull R) (s ∪ t)

theorem Convexity.IsConvexSet.sdiff_singleton_iff_notMem_convexHull {R : Type u_1} {X : Type u_2} [Semiring R] [PartialOrder R] [IsStrictOrderedRing R] [ConvexSpace R X] {s : Set X} {x : X} (hs : IsConvexSet R s) : IsConvexSet R (s \ {x}) ↔ x ∉ (convexHull R) (s \ {x})

theorem Convexity.IsAffineMap.image_convexHull {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} (hf : IsAffineMap R f) (s : Set X) : f '' (convexHull R) s = (convexHull R) (f '' s)