mathlib3
4705dd0d - split(analysis/convex/segment): Split off `analysis/convex.basic` (#16112)

Commit
3 years ago
split(analysis/convex/segment): Split off `analysis/convex.basic` (#16112) Move `segment` and `open_segment` to a new file `analysis.convex.segment`.
Author
Parents
Loading