Theorem norm_sum_lt_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 norm_sum_lt_of_strictConvexSpaceView on Github →