Documentation

Mathlib.Analysis.Convex.Topology

Topological properties of convex sets #

We prove the following facts:

source
theorem Real.convex_iff_isPreconnected {s : Set ℝ} :
Convex ℝ s ↔ IsPreconnected s
source
theorem IsPreconnected.convex {s : Set ℝ} :
IsPreconnected s → Convex ℝ s

Alias of the reverse direction of Real.convex_iff_isPreconnected.

Standard simplex #

source
theorem stdSimplex_subset_closedBall {ι : Type u_1} [Fintype ι] :
stdSimplex ℝ ι ⊆ Metric.closedBall 0 1

Every vector in stdSimplex 𝕜 ι has max-norm at most 1.

source
theorem bounded_stdSimplex (ι : Type u_1) [Fintype ι] :
Bornology.IsBounded (stdSimplex ℝ ι)

stdSimplex ℝ ι is bounded.

source
theorem isClosed_stdSimplex (ι : Type u_1) [Fintype ι] :
IsClosed (stdSimplex ℝ ι)

stdSimplex ℝ ι is closed.

source
theorem isCompact_stdSimplex (ι : Type u_1) [Fintype ι] :
IsCompact (stdSimplex ℝ ι)

stdSimplex ℝ ι is compact.

source
instance stdSimplex.instCompactSpace_coe (ι : Type u_1) [Fintype ι] :
CompactSpace ↑(stdSimplex ℝ ι)
Equations
source
@[simp]
theorem stdSimplexHomeomorphUnitInterval_symm_apply_coe (x : ↑(Set.Icc 0 1)) :
↑((Homeomorph.symm stdSimplexHomeomorphUnitInterval) x) = ![↑x, 1 - ↑x]
source
@[simp]
theorem stdSimplexHomeomorphUnitInterval_apply_coe (f : ↑(stdSimplex ℝ (Fin 2))) :
↑(stdSimplexHomeomorphUnitInterval f) = ↑f 0
source
def stdSimplexHomeomorphUnitInterval :
↑(stdSimplex ℝ (Fin 2)) ≃ₜ ↑unitInterval

The standard one-dimensional simplex in ℝ² = Fin 2 → ℝ is homeomorphic to the unit interval.

Equations
Instances For

    Topological vector space #

    source
    theorem segment_subset_closure_openSegment {𝕜 : Type u_2} {E : Type u_3} [LinearOrderedRing 𝕜] [DenselyOrdered 𝕜] [TopologicalSpace 𝕜] [OrderTopology 𝕜] [AddCommGroup E] [TopologicalSpace E] [ContinuousAdd E] [Module 𝕜 E] [ContinuousSMul 𝕜 E] {x : E} {y : E} :
    segment 𝕜 x y ⊆ closure (openSegment 𝕜 x y)
    source
    @[simp]
    theorem closure_openSegment {𝕜 : Type u_2} {E : Type u_3} [LinearOrderedRing 𝕜] [DenselyOrdered 𝕜] [PseudoMetricSpace 𝕜] [OrderTopology 𝕜] [ProperSpace 𝕜] [CompactIccSpace 𝕜] [AddCommGroup E] [TopologicalSpace E] [T2Space E] [ContinuousAdd E] [Module 𝕜 E] [ContinuousSMul 𝕜 E] (x : E) (y : E) :
    closure (openSegment 𝕜 x y) = segment 𝕜 x y
    source
    theorem Convex.combo_interior_closure_subset_interior {𝕜 : Type u_2} {E : Type u_3} [LinearOrderedField 𝕜] [AddCommGroup E] [Module 𝕜 E] [TopologicalSpace E] [TopologicalAddGroup E] [ContinuousConstSMul 𝕜 E] {s : Set E} (hs : Convex 𝕜 s) {a : 𝕜} {b : 𝕜} (ha : 0 < a) (hb : 0 ≤ b) (hab : a + b = 1) :
    a • interior s + b • closure s ⊆ interior s

    If s is a convex set, then a • interior s + b • closure s ⊆ interior s for all 0 < a, 0 ≤ b, a + b = 1. See also Convex.combo_interior_self_subset_interior for a weaker version.

    source
    theorem Convex.combo_interior_self_subset_interior {𝕜 : Type u_2} {E : Type u_3} [LinearOrderedField 𝕜] [AddCommGroup E] [Module 𝕜 E] [TopologicalSpace E] [TopologicalAddGroup E] [ContinuousConstSMul 𝕜 E] {s : Set E} (hs : Convex 𝕜 s) {a : 𝕜} {b : 𝕜} (ha : 0 < a) (hb : 0 ≤ b) (hab : a + b = 1) :
    a • interior s + b • s ⊆ interior s

    If s is a convex set, then a • interior s + b • s ⊆ interior s for all 0 < a, 0 ≤ b, a + b = 1. See also Convex.combo_interior_closure_subset_interior for a stronger version.

    source
    theorem Convex.combo_closure_interior_subset_interior {𝕜 : Type u_2} {E : Type u_3} [LinearOrderedField 𝕜] [AddCommGroup E] [Module 𝕜 E] [TopologicalSpace E] [TopologicalAddGroup E] [ContinuousConstSMul 𝕜 E] {s : Set E} (hs : Convex 𝕜 s) {a : 𝕜} {b : 𝕜} (ha : 0 ≤ a) (hb : 0 < b) (hab : a + b = 1) :
    a • closure s + b • interior s ⊆ interior s

    If s is a convex set, then a • closure s + b • interior s ⊆ interior s for all 0 ≤ a, 0 < b, a + b = 1. See also Convex.combo_self_interior_subset_interior for a weaker version.

    source
    theorem Convex.combo_self_interior_subset_interior {𝕜 : Type u_2} {E : Type u_3} [LinearOrderedField 𝕜] [AddCommGroup E] [Module 𝕜 E] [TopologicalSpace E] [TopologicalAddGroup E] [ContinuousConstSMul 𝕜 E] {s : Set E} (hs : Convex 𝕜 s) {a : 𝕜} {b : 𝕜} (ha : 0 ≤ a) (hb : 0 < b) (hab : a + b = 1) :
    a • s + b • interior s ⊆ interior s

    If s is a convex set, then a • s + b • interior s ⊆ interior s for all 0 ≤ a, 0 < b, a + b = 1. See also Convex.combo_closure_interior_subset_interior for a stronger version.

    source
    theorem Convex.combo_interior_closure_mem_interior {𝕜 : Type u_2} {E : Type u_3} [LinearOrderedField 𝕜] [AddCommGroup E] [Module 𝕜 E] [TopologicalSpace E] [TopologicalAddGroup E] [ContinuousConstSMul 𝕜 E] {s : Set E} (hs : Convex 𝕜 s) {x : E} {y : E} (hx : x ∈ interior s) (hy : y ∈ closure s) {a : 𝕜} {b : 𝕜} (ha : 0 < a) (hb : 0 ≤ b) (hab : a + b = 1) :
    a • x + b • y ∈ interior s
    source
    theorem Convex.combo_interior_self_mem_interior {𝕜 : Type u_2} {E : Type u_3} [LinearOrderedField 𝕜] [AddCommGroup E] [Module 𝕜 E] [TopologicalSpace E] [TopologicalAddGroup E] [ContinuousConstSMul 𝕜 E] {s : Set E} (hs : Convex 𝕜 s) {x : E} {y : E} (hx : x ∈ interior s) (hy : y ∈ s) {a : 𝕜} {b : 𝕜} (ha : 0 < a) (hb : 0 ≤ b) (hab : a + b = 1) :
    a • x + b • y ∈ interior s
    source
    theorem Convex.combo_closure_interior_mem_interior {𝕜 : Type u_2} {E : Type u_3} [LinearOrderedField 𝕜] [AddCommGroup E] [Module 𝕜 E] [TopologicalSpace E] [TopologicalAddGroup E] [ContinuousConstSMul 𝕜 E] {s : Set E} (hs : Convex 𝕜 s) {x : E} {y : E} (hx : x ∈ closure s) (hy : y ∈ interior s) {a : 𝕜} {b : 𝕜} (ha : 0 ≤ a) (hb : 0 < b) (hab : a + b = 1) :
    a • x + b • y ∈ interior s
    source
    theorem Convex.combo_self_interior_mem_interior {𝕜 : Type u_2} {E : Type u_3} [LinearOrderedField 𝕜] [AddCommGroup E] [Module 𝕜 E] [TopologicalSpace E] [TopologicalAddGroup E] [ContinuousConstSMul 𝕜 E] {s : Set E} (hs : Convex 𝕜 s) {x : E} {y : E} (hx : x ∈ s) (hy : y ∈ interior s) {a : 𝕜} {b : 𝕜} (ha : 0 ≤ a) (hb : 0 < b) (hab : a + b = 1) :
    a • x + b • y ∈ interior s
    source
    theorem Convex.openSegment_interior_closure_subset_interior {𝕜 : Type u_2} {E : Type u_3} [LinearOrderedField 𝕜] [AddCommGroup E] [Module 𝕜 E] [TopologicalSpace E] [TopologicalAddGroup E] [ContinuousConstSMul 𝕜 E] {s : Set E} (hs : Convex 𝕜 s) {x : E} {y : E} (hx : x ∈ interior s) (hy : y ∈ closure s) :
    openSegment 𝕜 x y ⊆ interior s
    source
    theorem Convex.openSegment_interior_self_subset_interior {𝕜 : Type u_2} {E : Type u_3} [LinearOrderedField 𝕜] [AddCommGroup E] [Module 𝕜 E] [TopologicalSpace E] [TopologicalAddGroup E] [ContinuousConstSMul 𝕜 E] {s : Set E} (hs : Convex 𝕜 s) {x : E} {y : E} (hx : x ∈ interior s) (hy : y ∈ s) :
    openSegment 𝕜 x y ⊆ interior s
    source
    theorem Convex.openSegment_closure_interior_subset_interior {𝕜 : Type u_2} {E : Type u_3} [LinearOrderedField 𝕜] [AddCommGroup E] [Module 𝕜 E] [TopologicalSpace E] [TopologicalAddGroup E] [ContinuousConstSMul 𝕜 E] {s : Set E} (hs : Convex 𝕜 s) {x : E} {y : E} (hx : x ∈ closure s) (hy : y ∈ interior s) :
    openSegment 𝕜 x y ⊆ interior s
    source
    theorem Convex.openSegment_self_interior_subset_interior {𝕜 : Type u_2} {E : Type u_3} [LinearOrderedField 𝕜] [AddCommGroup E] [Module 𝕜 E] [TopologicalSpace E] [TopologicalAddGroup E] [ContinuousConstSMul 𝕜 E] {s : Set E} (hs : Convex 𝕜 s) {x : E} {y : E} (hx : x ∈ s) (hy : y ∈ interior s) :
    openSegment 𝕜 x y ⊆ interior s
    source
    theorem Convex.add_smul_sub_mem_interior' {𝕜 : Type u_2} {E : Type u_3} [LinearOrderedField 𝕜] [AddCommGroup E] [Module 𝕜 E] [TopologicalSpace E] [TopologicalAddGroup E] [ContinuousConstSMul 𝕜 E] {s : Set E} (hs : Convex 𝕜 s) {x : E} {y : E} (hx : x ∈ closure s) (hy : y ∈ interior s) {t : 𝕜} (ht : t ∈ Set.Ioc 0 1) :
    x + t • (y - x) ∈ interior s

    If x ∈ closure s and y ∈ interior s, then the segment (x, y] is included in interior s.

    source
    theorem Convex.add_smul_sub_mem_interior {𝕜 : Type u_2} {E : Type u_3} [LinearOrderedField 𝕜] [AddCommGroup E] [Module 𝕜 E] [TopologicalSpace E] [TopologicalAddGroup E] [ContinuousConstSMul 𝕜 E] {s : Set E} (hs : Convex 𝕜 s) {x : E} {y : E} (hx : x ∈ s) (hy : y ∈ interior s) {t : 𝕜} (ht : t ∈ Set.Ioc 0 1) :
    x + t • (y - x) ∈ interior s

    If x ∈ s and y ∈ interior s, then the segment (x, y] is included in interior s.

    source
    theorem Convex.add_smul_mem_interior' {𝕜 : Type u_2} {E : Type u_3} [LinearOrderedField 𝕜] [AddCommGroup E] [Module 𝕜 E] [TopologicalSpace E] [TopologicalAddGroup E] [ContinuousConstSMul 𝕜 E] {s : Set E} (hs : Convex 𝕜 s) {x : E} {y : E} (hx : x ∈ closure s) (hy : x + y ∈ interior s) {t : 𝕜} (ht : t ∈ Set.Ioc 0 1) :
    x + t • y ∈ interior s

    If x ∈ closure s and x + y ∈ interior s, then x + t y ∈ interior s for t ∈ (0, 1].

    source
    theorem Convex.add_smul_mem_interior {𝕜 : Type u_2} {E : Type u_3} [LinearOrderedField 𝕜] [AddCommGroup E] [Module 𝕜 E] [TopologicalSpace E] [TopologicalAddGroup E] [ContinuousConstSMul 𝕜 E] {s : Set E} (hs : Convex 𝕜 s) {x : E} {y : E} (hx : x ∈ s) (hy : x + y ∈ interior s) {t : 𝕜} (ht : t ∈ Set.Ioc 0 1) :
    x + t • y ∈ interior s

    If x ∈ s and x + y ∈ interior s, then x + t y ∈ interior s for t ∈ (0, 1].

    source
    theorem Convex.interior {𝕜 : Type u_2} {E : Type u_3} [LinearOrderedField 𝕜] [AddCommGroup E] [Module 𝕜 E] [TopologicalSpace E] [TopologicalAddGroup E] [ContinuousConstSMul 𝕜 E] {s : Set E} (hs : Convex 𝕜 s) :
    Convex 𝕜 (interior s)

    In a topological vector space, the interior of a convex set is convex.

    source
    theorem Convex.closure {𝕜 : Type u_2} {E : Type u_3} [LinearOrderedField 𝕜] [AddCommGroup E] [Module 𝕜 E] [TopologicalSpace E] [TopologicalAddGroup E] [ContinuousConstSMul 𝕜 E] {s : Set E} (hs : Convex 𝕜 s) :
    Convex 𝕜 (closure s)

    In a topological vector space, the closure of a convex set is convex.

    source
    theorem Convex.strictConvex' {𝕜 : Type u_2} {E : Type u_3} [LinearOrderedField 𝕜] [AddCommGroup E] [Module 𝕜 E] [TopologicalSpace E] [TopologicalAddGroup E] [ContinuousConstSMul 𝕜 E] {s : Set E} (hs : Convex 𝕜 s) (h : Set.Pairwise (s \ interior s) fun (x y : E) => ∃ (c : 𝕜), (AffineMap.lineMap x y) c ∈ interior s) :
    StrictConvex 𝕜 s

    A convex set s is strictly convex provided that for any two distinct points of s \ interior s, the line passing through these points has nonempty intersection with interior s.

    source
    theorem Convex.strictConvex {𝕜 : Type u_2} {E : Type u_3} [LinearOrderedField 𝕜] [AddCommGroup E] [Module 𝕜 E] [TopologicalSpace E] [TopologicalAddGroup E] [ContinuousConstSMul 𝕜 E] {s : Set E} (hs : Convex 𝕜 s) (h : Set.Pairwise (s \ interior s) fun (x y : E) => Set.Nonempty (segment 𝕜 x y \ frontier s)) :
    StrictConvex 𝕜 s

    A convex set s is strictly convex provided that for any two distinct points x, y of s \ interior s, the segment with endpoints x, y has nonempty intersection with interior s.

    source
    theorem Set.Finite.isCompact_convexHull {E : Type u_3} [AddCommGroup E] [Module ℝ E] [TopologicalSpace E] [TopologicalAddGroup E] [ContinuousSMul ℝ E] {s : Set E} (hs : Set.Finite s) :
    IsCompact ((convexHull ℝ) s)

    Convex hull of a finite set is compact.

    source
    theorem Set.Finite.isClosed_convexHull {E : Type u_3} [AddCommGroup E] [Module ℝ E] [TopologicalSpace E] [TopologicalAddGroup E] [ContinuousSMul ℝ E] [T2Space E] {s : Set E} (hs : Set.Finite s) :
    IsClosed ((convexHull ℝ) s)

    Convex hull of a finite set is closed.

    source
    theorem Convex.closure_subset_image_homothety_interior_of_one_lt {E : Type u_3} [AddCommGroup E] [Module ℝ E] [TopologicalSpace E] [TopologicalAddGroup E] [ContinuousSMul ℝ E] {s : Set E} (hs : Convex ℝ s) {x : E} (hx : x ∈ interior s) (t : ℝ) (ht : 1 < t) :
    closure s ⊆ ⇑(AffineMap.homothety x t) '' interior s

    If we dilate the interior of a convex set about a point in its interior by a scale t > 1, the result includes the closure of the original set.

    TODO Generalise this from convex sets to sets that are balanced / star-shaped about x.

    source
    theorem Convex.closure_subset_interior_image_homothety_of_one_lt {E : Type u_3} [AddCommGroup E] [Module ℝ E] [TopologicalSpace E] [TopologicalAddGroup E] [ContinuousSMul ℝ E] {s : Set E} (hs : Convex ℝ s) {x : E} (hx : x ∈ interior s) (t : ℝ) (ht : 1 < t) :
    closure s ⊆ interior (⇑(AffineMap.homothety x t) '' s)

    If we dilate a convex set about a point in its interior by a scale t > 1, the interior of the result includes the closure of the original set.

    TODO Generalise this from convex sets to sets that are balanced / star-shaped about x.

    source
    theorem Convex.subset_interior_image_homothety_of_one_lt {E : Type u_3} [AddCommGroup E] [Module ℝ E] [TopologicalSpace E] [TopologicalAddGroup E] [ContinuousSMul ℝ E] {s : Set E} (hs : Convex ℝ s) {x : E} (hx : x ∈ interior s) (t : ℝ) (ht : 1 < t) :
    s ⊆ interior (⇑(AffineMap.homothety x t) '' s)

    If we dilate a convex set about a point in its interior by a scale t > 1, the interior of the result includes the closure of the original set.

    TODO Generalise this from convex sets to sets that are balanced / star-shaped about x.

    source
    theorem JoinedIn.of_segment_subset {E : Type u_4} [AddCommGroup E] [Module ℝ E] [TopologicalSpace E] [ContinuousAdd E] [ContinuousSMul ℝ E] {x : E} {y : E} {s : Set E} (h : segment ℝ x y ⊆ s) :
    JoinedIn s x y
    source
    theorem Convex.isPathConnected {E : Type u_3} [AddCommGroup E] [Module ℝ E] [TopologicalSpace E] [TopologicalAddGroup E] [ContinuousSMul ℝ E] {s : Set E} (hconv : Convex ℝ s) (hne : Set.Nonempty s) :
    IsPathConnected s

    A nonempty convex set is path connected.

    source
    theorem Convex.isConnected {E : Type u_3} [AddCommGroup E] [Module ℝ E] [TopologicalSpace E] [TopologicalAddGroup E] [ContinuousSMul ℝ E] {s : Set E} (h : Convex ℝ s) (hne : Set.Nonempty s) :
    IsConnected s

    A nonempty convex set is connected.

    source
    theorem Convex.isPreconnected {E : Type u_3} [AddCommGroup E] [Module ℝ E] [TopologicalSpace E] [TopologicalAddGroup E] [ContinuousSMul ℝ E] {s : Set E} (h : Convex ℝ s) :
    IsPreconnected s

    A convex set is preconnected.

    source
    theorem TopologicalAddGroup.pathConnectedSpace {E : Type u_3} [AddCommGroup E] [Module ℝ E] [TopologicalSpace E] [TopologicalAddGroup E] [ContinuousSMul ℝ E] :
    PathConnectedSpace E

    Every topological vector space over ℝ is path connected.

    Not an instance, because it creates enormous TC subproblems (turn on pp.all).