Theorem sum_mem_ball_of_strictConvexSpace

Modification history

2025-12-06 00:03
Mathlib/Analysis/Convex/StrictCombination.lean
feat(Analysis/Convex/StrictCombination): convex combinations in strictly convex sets and spaces (#31452) …
Added sum_mem_ball_of_strictConvexSpaceView on Github →