Structures · Analysis

Convexity.IsConvexDist

A convex metric space is a real convex space with a compatible metric structure. Concretely, we ask for dist(∑ tᵢ xᵢ, ∑ tᵢ yᵢ) ≤ ∑ tᵢ dist(xᵢ, yᵢ), which is what one would expect from the triangle inequality. In particular, convex subsets of normed affine spaces are convex metric spaces. Note that there is a separate notion of [convex metric spaces](https://en.wikipedia.org/wiki/Convex_metric_space) in the literature that has little to do with this definition.

Defined in

Mathlib.Analysis.Convex.MetricSpace

Shape

One type argument · adds dist_iConvexComb_fst_snd_le