Documentation

Mathlib.Geometry.Convex.Hull

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.

source
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
Instances For
    source
    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
    source
    @[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
    source
    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)
    source
    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
    source
    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
    source
    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
    source
    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
    source
    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
    source
    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
    source
    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
    source
    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.

    source
    @[simp]
    theorem Convexity.convexHull_empty (R : Type u_1) {X : Type u_2} [Semiring R] [PartialOrder R] [IsStrictOrderedRing R] [ConvexSpace R X] :
    (convexHull R) ∅ = ∅
    source
    @[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 = ∅
    source
    @[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
    source
    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.

    source
    @[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}
    source
    @[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
    source
    @[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}
    source
    @[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)
    source
    @[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)
    source
    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})
    source
    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)