Topological and metric 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.compact_convex_hull : convex hull of a finite set is compact;
set.finite.is_closed_convex_hull : convex hull of a finite set is closed;
convex_on_dist : distance to a fixed point is convex on any convex set;
convex_hull_ediam, convex_hull_diam : convex hull of a set has the same (e)metric diameter as the original set;
bounded_convex_hull : convex hull of a set is bounded if and only if the original set is bounded.
bounded_std_simplex, is_closed_std_simplex, compact_std_simplex: topological properties of the standard simplex;

source

theorem real.convex_iff_is_preconnected {s : set ℝ} :

convex s ↔ is_preconnected s

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 compact_std_simplex (ι : Type u_1) [fintype ι] :

is_compact (std_simplex ι)

std_simplex ι is compact.

Topological vector space

source

theorem convex.interior {E : Type u_2} [add_comm_group E] [vector_space ℝ E] [topological_space E] [topological_add_group E] [topological_vector_space ℝ E] {s : set E} :

convex s → convex (interior s)

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

source

theorem convex.closure {E : Type u_2} [add_comm_group E] [vector_space ℝ E] [topological_space E] [topological_add_group E] [topological_vector_space ℝ E] {s : set E} :

convex s → convex (closure s)

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

source

theorem set.finite.compact_convex_hull {E : Type u_2} [add_comm_group E] [vector_space ℝ E] [topological_space E] [topological_add_group E] [topological_vector_space ℝ E] {s : set E} :

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_2} [add_comm_group E] [vector_space ℝ E] [topological_space E] [topological_add_group E] [topological_vector_space ℝ E] [t2_space E] {s : set E} :

s.finite → is_closed (convex_hull s)

Convex hull of a finite set is closed.

Normed vector space

source

theorem convex_on_dist {E : Type u_2} [normed_group E] [normed_space ℝ E] (z : E) (s : set E) :

convex s → convex_on s (λ (z' : E), has_dist.dist z' z)

source

theorem convex_ball {E : Type u_2} [normed_group E] [normed_space ℝ E] (a : E) (r : ℝ) :

convex (metric.ball a r)

source

theorem convex_closed_ball {E : Type u_2} [normed_group E] [normed_space ℝ E] (a : E) (r : ℝ) :

convex (metric.closed_ball a r)

source

theorem convex_hull_exists_dist_ge {E : Type u_2} [normed_group E] [normed_space ℝ E] {s : set E} {x : E} (hx : x ∈ convex_hull s) (y : E) :

∃ (x' : E) (H : x' ∈ s), has_dist.dist x y ≤ has_dist.dist x' y

Given a point x in the convex hull of s and a point y, there exists a point of s at distance at least dist x y from y.

source

theorem convex_hull_exists_dist_ge2 {E : Type u_2} [normed_group E] [normed_space ℝ E] {s t : set E} {x y : E} :

x ∈ convex_hull s → y ∈ convex_hull t → (∃ (x' : E) (H : x' ∈ s) (y' : E) (H : y' ∈ t), has_dist.dist x y ≤ has_dist.dist x' y')

Given a point x in the convex hull of s and a point y in the convex hull of t, there exist points x' ∈ s and y' ∈ t at distance at least dist x y.

source

@[simp]