Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2023-03-01 12:30 c5773405

View on Github →

feat(analysis/convex/extreme): Extreme points of s ×ˢ t (#18171) Characterise segment, open_segment, extreme_points in prod and pi.

Estimated changes

Modified src/analysis/convex/extreme.lean

deleted theorem extreme_points_def

added theorem extreme_points_pi

added theorem extreme_points_prod

modified theorem is_extreme_Inter

modified theorem is_extreme_bInter

added theorem mem_extreme_points

Modified src/analysis/convex/segment.lean

added theorem image_open_segment

added theorem image_segment

modified theorem mem_segment_translate

deleted theorem open_segment_image

added theorem pi.image_update_open_segment

added theorem pi.image_update_segment

added theorem pi.open_segment_subset

added theorem pi.segment_subset

added theorem prod.image_mk_open_segment_left

added theorem prod.image_mk_open_segment_right

added theorem prod.image_mk_segment_left

added theorem prod.image_mk_segment_right

added theorem prod.open_segment_subset

added theorem prod.segment_subset

deleted theorem segment_image

added theorem vadd_open_segment

added theorem vadd_segment