Theorems · Theorem · general topology

Convexity.dist_convexCombination_right_le

Deprecated since 2026-05-15Use Convexity.dist_iConvexComb_le instead.

∀ {X : Type u_2} [inst : Convexity.ConvexSpace ℝ X] [inst_1 : MetricSpace X] [Convexity.IsConvexDist X] {ι : Type u_3}
  (f : Convexity.StdSimplex ℝ ι) (x y : ι → X),
  dist (Convexity.iConvexComb f x) (Convexity.iConvexComb f y) ≤ Convexity.iConvexComb f fun i => dist (x i) (y i)

Alias of Convexity.dist_iConvexComb_le. dist(∑ tᵢ xᵢ, ∑ tᵢ yᵢ) ≤ ∑ tᵢ dist(xᵢ, yᵢ)

Defined in

Mathlib.Analysis.Convex.MetricSpace

Cited by

0 results in Mathlib

Foundations

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

Assumes

Convexity.ConvexSpaceMetricSpaceConvexity.IsConvexDist