Mathlib Changelog
v3
Changelog
About
Github
Mathlib v3 is deprecated.
Go to Mathlib v4
Commit
2021-12-13 09:36
fb819501
View on Github →
feat(analysis/convex/basic): lemmas about midpoint and segment (
#10682
)
Estimated changes
Modified
src/analysis/convex/basic.lean
added
theorem
mem_segment_add_sub
added
theorem
mem_segment_sub_add
added
theorem
midpoint_mem_segment
Modified
src/linear_algebra/affine_space/midpoint.lean
added
theorem
midpoint_add_sub
added
theorem
midpoint_neg_self
added
theorem
midpoint_self_neg
added
theorem
midpoint_sub_add