Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2021-09-10 18:48 7500529f

View on Github →

refactor(analysis/convex/basic): generalize segments to vector spaces (#9094) segment and open_segment are currently only defined in real vector spaces. This generalizes ℝ to arbitrary ordered_semirings in definitions and abstracts it away to the correct generality in lemmas. It also generalizes the space from add_comm_group to add_comm_monoid where possible.

Estimated changes

added theorem Icc_subset_segment
modified theorem convex.add
modified theorem convex.combo_self
modified theorem convex.mem_Icc
modified theorem convex.mem_Ico
modified theorem convex.mem_Ioc
modified theorem convex.mem_Ioo
modified theorem convex.segment_subset
modified theorem convex.sub
modified theorem convex_empty
modified theorem convex_open_segment
modified theorem convex_segment
modified theorem left_mem_open_segment_iff
modified theorem left_mem_segment
modified theorem mem_segment_translate
modified def open_segment
modified theorem open_segment_eq_Ioo'
modified theorem open_segment_eq_Ioo
modified theorem open_segment_image
modified theorem right_mem_segment
modified def segment
modified theorem segment_eq_Icc'
modified theorem segment_eq_Icc
modified theorem segment_eq_image'
modified theorem segment_eq_image
modified theorem segment_eq_interval
modified theorem segment_image
modified theorem segment_same
added theorem segment_subset_Icc
modified theorem segment_symm
modified theorem segment_translate_image
modified theorem segment_translate_preimage