Theorems · Theorem · general topology

Convexity.dist_iConvexComb_left_le

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

Defined in

Mathlib.Analysis.Convex.MetricSpace

Cited by

1 results in Mathlib

Foundations

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

Assumes

Convexity.ConvexSpaceMetricSpaceConvexity.IsConvexDist