Theorems · Theorem · general topology

Convexity.IsConvexDist.dist_iConvexComb_fst_snd_le

∀ {X : Type u_2} [inst₁ : Convexity.ConvexSpace ℝ X] [inst₂ : MetricSpace X] [self : Convexity.IsConvexDist X]
  (f : Convexity.StdSimplex ℝ (X × X)),
  dist (Convexity.iConvexComb f Prod.fst) (Convexity.iConvexComb f Prod.snd) ≤
    Convexity.iConvexComb f fun x => dist x.1 x.2

Use dist_iConvexComb_le instead.

Defined in: Mathlib.Analysis.Convex.MetricSpace
Cited by: 1 results in Mathlib
Foundations: Depth 105 from the axioms · uses propext, Classical.choice, Quot.sound
Assumes: Convexity.ConvexSpace MetricSpace Convexity.IsConvexDist

Mathlib docs Source Loogle LeanSearch

Around this declaration

Dashed lines are statement dependencies; solid lines are citations in proofs.

Cites7

Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.

Realstatement and proof · cited by 25,697
MetricSpacestatement and proof · cited by 1,684
Dist.diststatement · cited by 1,539
Convexity.ConvexSpacestatement and proof · cited by 176
Convexity.StdSimplexstatement · cited by 123
Convexity.iConvexCombstatement · cited by 51
Convexity.IsConvexDiststatement and proof · cited by 18

Cited by1

Results whose statement or proof uses this declaration.

Convexity.dist_iConvexComb_leproof · cited by 5