Commit 2024-10-02 12:24 4236727d

View on Github →

feat: a ball in ℝ is a segment (#17282) From LeanCamCombi

Estimated changes

Modified Mathlib/Analysis/Convex/Topology.lean

added theorem Real.ball_eq_openSegment

added theorem Real.closedBall_eq_segment

modified theorem Real.convex_iff_isPreconnected