Theorems · Inductive type · general topology

Convexity.IsConvexDist

(X : Type u_2) → [inst₁ : Convexity.ConvexSpace ℝ X] → [inst₂ : MetricSpace X] → Prop

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

Cited by

18 results in Mathlib

Foundations

Depth 104 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

Convexity.ConvexSpaceMetricSpace