mathlib

c5773405 - feat(analysis/convex/extreme): Extreme points of `s ×ˢ t` (#18171)

feat(analysis/convex/extreme): Extreme points of `s ×ˢ t` (#18171) Characterise `segment`, `open_segment`, `extreme_points` in `prod` and `pi`. Co-authored-by: Eric Wieser <wieser.eric@gmail.com>