Theorem convex_closedBall

Modification history

2026-02-09 08:58

Mathlib/Analysis/Normed/Module/Convex.lean

feat: segment is contained in closed ball (#34860)

Modified convex_closedBall View on Github →

2023-04-24 22:52

Mathlib/Analysis/Convex/Normed.lean

feat: port Analysis.Convex.Normed (#3626)

Added convex_closedBall View on Github →