mathlib3 documentation

analysis.convex.topology

Topological properties of convex sets #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

We prove the following facts:

source
theorem real.convex_iff_is_preconnected {s : set ℝ} :
convex ℝ s ↔ is_preconnected s
source
theorem is_preconnected.convex {s : set ℝ} :
is_preconnected s → convex ℝ s

Alias of the reverse direction of real.convex_iff_is_preconnected.

Standard simplex #

source
theorem std_simplex_subset_closed_ball {ι : Type u_1} [fintype ι] :
std_simplex ℝ ι ⊆ metric.closed_ball 0 1

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

source
theorem bounded_std_simplex (ι : Type u_1) [fintype ι] :
metric.bounded (std_simplex ℝ ι)

std_simplex ℝ ι is bounded.

source
theorem is_closed_std_simplex (ι : Type u_1) [fintype ι] :
is_closed (std_simplex ℝ ι)

std_simplex ℝ ι is closed.

source
theorem is_compact_std_simplex (ι : Type u_1) [fintype ι] :
is_compact (std_simplex ℝ ι)

std_simplex ℝ ι is compact.

Topological vector space #

source
theorem segment_subset_closure_open_segment {𝕜 : Type u_2} {E : Type u_3} [linear_ordered_ring 𝕜] [densely_ordered 𝕜] [topological_space 𝕜] [order_topology 𝕜] [add_comm_group E] [topological_space E] [has_continuous_add E] [module 𝕜 E] [has_continuous_smul 𝕜 E] {x y : E} :
segment 𝕜 x y ⊆ closure (open_segment 𝕜 x y)
source
@[simp]
theorem closure_open_segment {𝕜 : Type u_2} {E : Type u_3} [linear_ordered_ring 𝕜] [densely_ordered 𝕜] [pseudo_metric_space 𝕜] [order_topology 𝕜] [proper_space 𝕜] [compact_Icc_space 𝕜] [add_comm_group E] [topological_space E] [t2_space E] [has_continuous_add E] [module 𝕜 E] [has_continuous_smul 𝕜 E] (x y : E) :
closure (open_segment 𝕜 x y) = segment 𝕜 x y
source
theorem convex.combo_interior_closure_subset_interior {𝕜 : Type u_2} {E : Type u_3} [linear_ordered_field 𝕜] [add_comm_group E] [module 𝕜 E] [topological_space E] [topological_add_group E] [has_continuous_const_smul 𝕜 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} [linear_ordered_field 𝕜] [add_comm_group E] [module 𝕜 E] [topological_space E] [topological_add_group E] [has_continuous_const_smul 𝕜 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} [linear_ordered_field 𝕜] [add_comm_group E] [module 𝕜 E] [topological_space E] [topological_add_group E] [has_continuous_const_smul 𝕜 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} [linear_ordered_field 𝕜] [add_comm_group E] [module 𝕜 E] [topological_space E] [topological_add_group E] [has_continuous_const_smul 𝕜 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} [linear_ordered_field 𝕜] [add_comm_group E] [module 𝕜 E] [topological_space E] [topological_add_group E] [has_continuous_const_smul 𝕜 E] {s : set E} (hs : convex 𝕜 s) {x 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} [linear_ordered_field 𝕜] [add_comm_group E] [module 𝕜 E] [topological_space E] [topological_add_group E] [has_continuous_const_smul 𝕜 E] {s : set E} (hs : convex 𝕜 s) {x 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} [linear_ordered_field 𝕜] [add_comm_group E] [module 𝕜 E] [topological_space E] [topological_add_group E] [has_continuous_const_smul 𝕜 E] {s : set E} (hs : convex 𝕜 s) {x 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} [linear_ordered_field 𝕜] [add_comm_group E] [module 𝕜 E] [topological_space E] [topological_add_group E] [has_continuous_const_smul 𝕜 E] {s : set E} (hs : convex 𝕜 s) {x 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.open_segment_interior_closure_subset_interior {𝕜 : Type u_2} {E : Type u_3} [linear_ordered_field 𝕜] [add_comm_group E] [module 𝕜 E] [topological_space E] [topological_add_group E] [has_continuous_const_smul 𝕜 E] {s : set E} (hs : convex 𝕜 s) {x y : E} (hx : x ∈ interior s) (hy : y ∈ closure s) :
open_segment 𝕜 x y ⊆ interior s
source
theorem convex.open_segment_interior_self_subset_interior {𝕜 : Type u_2} {E : Type u_3} [linear_ordered_field 𝕜] [add_comm_group E] [module 𝕜 E] [topological_space E] [topological_add_group E] [has_continuous_const_smul 𝕜 E] {s : set E} (hs : convex 𝕜 s) {x y : E} (hx : x ∈ interior s) (hy : y ∈ s) :
open_segment 𝕜 x y ⊆ interior s
source
theorem convex.open_segment_closure_interior_subset_interior {𝕜 : Type u_2} {E : Type u_3} [linear_ordered_field 𝕜] [add_comm_group E] [module 𝕜 E] [topological_space E] [topological_add_group E] [has_continuous_const_smul 𝕜 E] {s : set E} (hs : convex 𝕜 s) {x y : E} (hx : x ∈ closure s) (hy : y ∈ interior s) :
open_segment 𝕜 x y ⊆ interior s
source
theorem convex.open_segment_self_interior_subset_interior {𝕜 : Type u_2} {E : Type u_3} [linear_ordered_field 𝕜] [add_comm_group E] [module 𝕜 E] [topological_space E] [topological_add_group E] [has_continuous_const_smul 𝕜 E] {s : set E} (hs : convex 𝕜 s) {x y : E} (hx : x ∈ s) (hy : y ∈ interior s) :
open_segment 𝕜 x y ⊆ interior s
source
theorem convex.add_smul_sub_mem_interior' {𝕜 : Type u_2} {E : Type u_3} [linear_ordered_field 𝕜] [add_comm_group E] [module 𝕜 E] [topological_space E] [topological_add_group E] [has_continuous_const_smul 𝕜 E] {s : set E} (hs : convex 𝕜 s) {x 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} [linear_ordered_field 𝕜] [add_comm_group E] [module 𝕜 E] [topological_space E] [topological_add_group E] [has_continuous_const_smul 𝕜 E] {s : set E} (hs : convex 𝕜 s) {x 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} [linear_ordered_field 𝕜] [add_comm_group E] [module 𝕜 E] [topological_space E] [topological_add_group E] [has_continuous_const_smul 𝕜 E] {s : set E} (hs : convex 𝕜 s) {x 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} [linear_ordered_field 𝕜] [add_comm_group E] [module 𝕜 E] [topological_space E] [topological_add_group E] [has_continuous_const_smul 𝕜 E] {s : set E} (hs : convex 𝕜 s) {x 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
@[protected]
theorem convex.interior {𝕜 : Type u_2} {E : Type u_3} [linear_ordered_field 𝕜] [add_comm_group E] [module 𝕜 E] [topological_space E] [topological_add_group E] [has_continuous_const_smul 𝕜 E] {s : set E} (hs : convex 𝕜 s) :
convex 𝕜 (interior s)

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

source
@[protected]
theorem convex.closure {𝕜 : Type u_2} {E : Type u_3} [linear_ordered_field 𝕜] [add_comm_group E] [module 𝕜 E] [topological_space E] [topological_add_group E] [has_continuous_const_smul 𝕜 E] {s : set E} (hs : convex 𝕜 s) :
convex 𝕜 (closure s)

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

source
@[protected]
theorem convex.strict_convex' {𝕜 : Type u_2} {E : Type u_3} [linear_ordered_field 𝕜] [add_comm_group E] [module 𝕜 E] [topological_space E] [topological_add_group E] [has_continuous_const_smul 𝕜 E] {s : set E} (hs : convex 𝕜 s) (h : (s \ interior s).pairwise (λ (x y : E), ∃ (c : 𝕜), ⇑(affine_map.line_map x y) c ∈ interior s)) :
strict_convex 𝕜 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
@[protected]
theorem convex.strict_convex {𝕜 : Type u_2} {E : Type u_3} [linear_ordered_field 𝕜] [add_comm_group E] [module 𝕜 E] [topological_space E] [topological_add_group E] [has_continuous_const_smul 𝕜 E] {s : set E} (hs : convex 𝕜 s) (h : (s \ interior s).pairwise (λ (x y : E), (segment 𝕜 x y \ frontier s).nonempty)) :
strict_convex 𝕜 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.compact_convex_hull {E : Type u_3} [add_comm_group E] [module ℝ E] [topological_space E] [topological_add_group E] [has_continuous_smul ℝ E] {s : set E} (hs : s.finite) :
is_compact (⇑(convex_hull ℝ) s)

Convex hull of a finite set is compact.

source
theorem set.finite.is_closed_convex_hull {E : Type u_3} [add_comm_group E] [module ℝ E] [topological_space E] [topological_add_group E] [has_continuous_smul ℝ E] [t2_space E] {s : set E} (hs : s.finite) :
is_closed (⇑(convex_hull ℝ) s)

Convex hull of a finite set is closed.

source
theorem convex.closure_subset_image_homothety_interior_of_one_lt {E : Type u_3} [add_comm_group E] [module ℝ E] [topological_space E] [topological_add_group E] [has_continuous_smul ℝ E] {s : set E} (hs : convex ℝ s) {x : E} (hx : x ∈ interior s) (t : ℝ) (ht : 1 < t) :
closure s ⊆ ⇑(affine_map.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} [add_comm_group E] [module ℝ E] [topological_space E] [topological_add_group E] [has_continuous_smul ℝ E] {s : set E} (hs : convex ℝ s) {x : E} (hx : x ∈ interior s) (t : ℝ) (ht : 1 < t) :
closure s ⊆ interior (⇑(affine_map.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} [add_comm_group E] [module ℝ E] [topological_space E] [topological_add_group E] [has_continuous_smul ℝ E] {s : set E} (hs : convex ℝ s) {x : E} (hx : x ∈ interior s) (t : ℝ) (ht : 1 < t) :
s ⊆ interior (⇑(affine_map.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
@[protected]
theorem convex.is_path_connected {E : Type u_3} [add_comm_group E] [module ℝ E] [topological_space E] [topological_add_group E] [has_continuous_smul ℝ E] {s : set E} (hconv : convex ℝ s) (hne : s.nonempty) :
is_path_connected s

A nonempty convex set is path connected.

source
@[protected]
theorem convex.is_connected {E : Type u_3} [add_comm_group E] [module ℝ E] [topological_space E] [topological_add_group E] [has_continuous_smul ℝ E] {s : set E} (h : convex ℝ s) (hne : s.nonempty) :
is_connected s

A nonempty convex set is connected.

source
@[protected]
theorem convex.is_preconnected {E : Type u_3} [add_comm_group E] [module ℝ E] [topological_space E] [topological_add_group E] [has_continuous_smul ℝ E] {s : set E} (h : convex ℝ s) :
is_preconnected s

A convex set is preconnected.

source
@[protected]
theorem topological_add_group.path_connected {E : Type u_3} [add_comm_group E] [module ℝ E] [topological_space E] [topological_add_group E] [has_continuous_smul ℝ E] :
path_connected_space E

Every topological vector space over ℝ is path connected.

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