Documentation

Mathlib.Analysis.Convex.Normed

Topological and metric properties of convex sets in normed spaces #

We prove the following facts:

theorem convexOn_norm {E : Type u_2} [SeminormedAddCommGroup E] [NormedSpace E] {s : Set E} (hs : Convex s) :
ConvexOn s norm

The norm on a real normed space is convex on any convex set. See also Seminorm.convexOn and convexOn_univ_norm.

theorem convexOn_univ_norm {E : Type u_2} [SeminormedAddCommGroup E] [NormedSpace E] :
ConvexOn Set.univ norm

The norm on a real normed space is convex on the whole space. See also Seminorm.convexOn and convexOn_norm.

theorem convexOn_dist {E : Type u_2} [SeminormedAddCommGroup E] [NormedSpace E] {s : Set E} (z : E) (hs : Convex s) :
ConvexOn s fun (z' : E) => dist z' z
theorem convexOn_univ_dist {E : Type u_2} [SeminormedAddCommGroup E] [NormedSpace E] (z : E) :
ConvexOn Set.univ fun (z' : E) => dist z' z
theorem convex_ball {E : Type u_2} [SeminormedAddCommGroup E] [NormedSpace E] (a : E) (r : ) :
theorem convexHull_exists_dist_ge {E : Type u_2} [SeminormedAddCommGroup E] [NormedSpace E] {s : Set E} {x : E} (hx : x (convexHull ) s) (y : E) :
x's, dist x y 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.

theorem convexHull_exists_dist_ge2 {E : Type u_2} [SeminormedAddCommGroup E] [NormedSpace E] {s : Set E} {t : Set E} {x : E} {y : E} (hx : x (convexHull ) s) (hy : y (convexHull ) t) :
x's, y't, dist x y 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.

@[simp]

Emetric diameter of the convex hull of a set s equals the emetric diameter of s.

@[simp]

Diameter of the convex hull of a set s equals the emetric diameter of s.

@[simp]

Convex hull of s is bounded if and only if s is bounded.

@[instance 100]
Equations
  • =
theorem Wbtw.dist_add_dist {E : Type u_2} {P : Type u_3} [SeminormedAddCommGroup E] [NormedSpace E] [PseudoMetricSpace P] [NormedAddTorsor E P] {x : P} {y : P} {z : P} (h : Wbtw x y z) :
dist x y + dist y z = dist x z
theorem dist_add_dist_of_mem_segment {E : Type u_2} [SeminormedAddCommGroup E] [NormedSpace E] {x : E} {y : E} {z : E} (h : y segment x z) :
dist x y + dist y z = dist x z

The set of vectors in the same ray as x is connected.

theorem isConnected_setOf_sameRay_and_ne_zero {E : Type u_2} [SeminormedAddCommGroup E] [NormedSpace E] {x : E} (hx : x 0) :
IsConnected {y : E | SameRay x y y 0}

The set of nonzero vectors in the same ray as the nonzero vector x is connected.

We can intercalate a simplex between a point and one of its neighborhoods.