Commit 2026-03-24 10:49 9e58132d

View on Github →

feat(Analysis/Convex): convex metric spaces (#36959)

Estimated changes

Modified Mathlib.lean

Created Mathlib/Analysis/Convex/MetricSpace.lean

added theorem ConvexSpace.ofConvex.coe_convexCombination

added theorem IsConvexMetricSpace.of_convex

added theorem continuous_convexComboPair'

added theorem continuous_convexComboPair

added theorem continuous_convexComboPair_of_isBounded

added theorem dist_convexCombination_left_le

added theorem dist_convexCombination_map_le

added theorem dist_convexCombination_right_le

added theorem dist_convexComboPair_convexComboPair

added theorem dist_convexComboPair_convexComboPair_le

added theorem dist_convexComboPair_left

added theorem dist_convexComboPair_right

added theorem dist_left_convexComboPair

added theorem dist_right_convexComboPair

Modified Mathlib/LinearAlgebra/ConvexSpace.lean

added theorem StdSimplex.map_comp

added theorem StdSimplex.map_const

added theorem StdSimplex.map_duple

added theorem StdSimplex.map_id

added theorem StdSimplex.map_map

added theorem StdSimplex.map_single

added theorem StdSimplex.nonempty

added theorem convexComboPair_symm

Modified Mathlib/LinearAlgebra/ConvexSpace/AffineSpace.lean

Modified Mathlib/Topology/MetricSpace/Bounded.lean