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_norm
,convex_on_dist
: norm and distance to a fixed point is convex on any convex set;convex_on_univ_norm
,convex_on_univ_dist
: norm and distance to a fixed point is convex on the whole space;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;
Alias of the reverse direction of real.convex_iff_is_preconnected
.
Standard simplex #
Every vector in std_simplex 𝕜 ι
has max
-norm at most 1
.
std_simplex ℝ ι
is bounded.
std_simplex ℝ ι
is closed.
std_simplex ℝ ι
is compact.
Topological vector space #
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.
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.
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.
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.
If x ∈ closure s
and y ∈ interior s
, then the segment (x, y]
is included in interior s
.
If x ∈ s
and y ∈ interior s
, then the segment (x, y]
is included in interior s
.
If x ∈ closure s
and x + y ∈ interior s
, then x + t y ∈ interior s
for t ∈ (0, 1]
.
If x ∈ s
and x + y ∈ interior s
, then x + t y ∈ interior s
for t ∈ (0, 1]
.
In a topological vector space, the interior of a convex set is convex.
In a topological vector space, the closure of a convex set is convex.
Convex hull of a finite set is compact.
Convex hull of a finite set is closed.
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
.
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
.
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
.
A nonempty convex set is path connected.
A nonempty convex set is connected.
A convex set is preconnected.
Every topological vector space over ℝ is path connected.
Not an instance, because it creates enormous TC subproblems (turn on pp.all
).
Normed vector space #
The norm on a real normed space is convex on any convex set. See also seminorm.convex_on
and convex_on_univ_norm
.
The norm on a real normed space is convex on the whole space. See also seminorm.convex_on
and convex_on_norm
.
If s
, t
are disjoint convex sets, s
is compact and t
is closed then we can find open
disjoint convex sets containing them.
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
.
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
.
Emetric diameter of the convex hull of a set s
equals the emetric diameter of `s.
Diameter of the convex hull of a set s
equals the emetric diameter of `s.
Convex hull of s
is bounded if and only if s
is bounded.