# Documentation

Mathlib.Analysis.Convex.Topology

# Topological properties of convex sets #

We prove the following facts:

• Convex.interior : interior of a convex set is convex;
• Convex.closure : closure of a convex set is convex;
• Set.Finite.isCompact_convexHull : convex hull of a finite set is compact;
• Set.Finite.isClosed_convexHull : convex hull of a finite set is closed.
theorem IsPreconnected.convex {s : } :

Alias of the reverse direction of Real.convex_iff_isPreconnected.

### Standard simplex #

theorem stdSimplex_subset_closedBall {ι : Type u_1} [] :

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

theorem bounded_stdSimplex (ι : Type u_1) [] :

stdSimplex ℝ ι is bounded.

theorem isClosed_stdSimplex (ι : Type u_1) [] :

stdSimplex ℝ ι is closed.

theorem isCompact_stdSimplex (ι : Type u_1) [] :

stdSimplex ℝ ι is compact.

### Topological vector space #

theorem segment_subset_closure_openSegment {𝕜 : Type u_2} {E : Type u_3} [] [] [] [] [] [] [Module 𝕜 E] [] {x : E} {y : E} :
segment 𝕜 x y closure (openSegment 𝕜 x y)
@[simp]
theorem closure_openSegment {𝕜 : Type u_2} {E : Type u_3} [] [] [] [] [] [] [] [] [Module 𝕜 E] [] (x : E) (y : E) :
closure (openSegment 𝕜 x y) = segment 𝕜 x y
theorem Convex.combo_interior_closure_subset_interior {𝕜 : Type u_2} {E : Type u_3} [] [Module 𝕜 E] [] [] {s : Set E} (hs : Convex 𝕜 s) {a : 𝕜} {b : 𝕜} (ha : 0 < a) (hb : 0 b) (hab : a + b = 1) :
a + b

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.

theorem Convex.combo_interior_self_subset_interior {𝕜 : Type u_2} {E : Type u_3} [] [Module 𝕜 E] [] [] {s : Set E} (hs : Convex 𝕜 s) {a : 𝕜} {b : 𝕜} (ha : 0 < a) (hb : 0 b) (hab : a + b = 1) :
a + b 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.

theorem Convex.combo_closure_interior_subset_interior {𝕜 : Type u_2} {E : Type u_3} [] [Module 𝕜 E] [] [] {s : Set E} (hs : Convex 𝕜 s) {a : 𝕜} {b : 𝕜} (ha : 0 a) (hb : 0 < b) (hab : a + b = 1) :
a + b

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.

theorem Convex.combo_self_interior_subset_interior {𝕜 : Type u_2} {E : Type u_3} [] [Module 𝕜 E] [] [] {s : Set E} (hs : Convex 𝕜 s) {a : 𝕜} {b : 𝕜} (ha : 0 a) (hb : 0 < b) (hab : a + b = 1) :
a s + b

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.

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

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

theorem Convex.add_smul_sub_mem_interior {𝕜 : Type u_2} {E : Type u_3} [] [Module 𝕜 E] [] [] {s : Set E} (hs : Convex 𝕜 s) {x : E} {y : E} (hx : x s) (hy : y ) {t : 𝕜} (ht : t Set.Ioc 0 1) :
x + t (y - x)

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

theorem Convex.add_smul_mem_interior' {𝕜 : Type u_2} {E : Type u_3} [] [Module 𝕜 E] [] [] {s : Set E} (hs : Convex 𝕜 s) {x : E} {y : E} (hx : x ) (hy : x + y ) {t : 𝕜} (ht : t Set.Ioc 0 1) :
x + t y

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

theorem Convex.add_smul_mem_interior {𝕜 : Type u_2} {E : Type u_3} [] [Module 𝕜 E] [] [] {s : Set E} (hs : Convex 𝕜 s) {x : E} {y : E} (hx : x s) (hy : x + y ) {t : 𝕜} (ht : t Set.Ioc 0 1) :
x + t y

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

theorem Convex.interior {𝕜 : Type u_2} {E : Type u_3} [] [Module 𝕜 E] [] [] {s : Set E} (hs : Convex 𝕜 s) :
Convex 𝕜 ()

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

theorem Convex.closure {𝕜 : Type u_2} {E : Type u_3} [] [Module 𝕜 E] [] [] {s : Set E} (hs : Convex 𝕜 s) :
Convex 𝕜 ()

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

theorem Convex.strictConvex' {𝕜 : Type u_2} {E : Type u_3} [] [Module 𝕜 E] [] [] {s : Set E} (hs : Convex 𝕜 s) (h : Set.Pairwise (s \ ) fun x y => c, ↑() c ) :

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.

theorem Convex.strictConvex {𝕜 : Type u_2} {E : Type u_3} [] [Module 𝕜 E] [] [] {s : Set E} (hs : Convex 𝕜 s) (h : Set.Pairwise (s \ ) fun x y => Set.Nonempty (segment 𝕜 x y \ )) :

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.

theorem Set.Finite.isCompact_convexHull {E : Type u_3} [] [] [] [] {s : Set E} (hs : ) :
IsCompact (↑() s)

Convex hull of a finite set is compact.

theorem Set.Finite.isClosed_convexHull {E : Type u_3} [] [] [] [] [] {s : Set E} (hs : ) :
IsClosed (↑() s)

Convex hull of a finite set is closed.

theorem Convex.closure_subset_image_homothety_interior_of_one_lt {E : Type u_3} [] [] [] [] {s : Set E} (hs : ) {x : E} (hx : x ) (t : ) (ht : 1 < t) :
↑() ''

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.

theorem Convex.closure_subset_interior_image_homothety_of_one_lt {E : Type u_3} [] [] [] [] {s : Set E} (hs : ) {x : E} (hx : x ) (t : ) (ht : 1 < t) :
interior (↑() '' 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.

theorem Convex.subset_interior_image_homothety_of_one_lt {E : Type u_3} [] [] [] [] {s : Set E} (hs : ) {x : E} (hx : x ) (t : ) (ht : 1 < t) :
s interior (↑() '' 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.

theorem JoinedIn_of_segment_subset {E : Type u_4} [] [] [] [] [] {x : E} {y : E} {s : Set E} (h : segment x y s) :
JoinedIn s x y
theorem Convex.isPathConnected {E : Type u_3} [] [] [] [] {s : Set E} (hconv : ) (hne : ) :

A nonempty convex set is path connected.

theorem Convex.isConnected {E : Type u_3} [] [] [] [] {s : Set E} (h : ) (hne : ) :

A nonempty convex set is connected.

theorem Convex.isPreconnected {E : Type u_3} [] [] [] [] {s : Set E} (h : ) :

A convex set is preconnected.

theorem TopologicalAddGroup.pathConnectedSpace {E : Type u_3} [] [] [] [] :

Every topological vector space over ℝ is path connected.

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