Commit 2026-03-06 16:20 e067b0fd

View on Github →

feat: midpoint_mem_openSegment (#36237) This lemma already exsited for segment, I am simply writing the openSegment version of it (and the two following lemmas)

Estimated changes

Modified Mathlib/Algebra/Order/Invertible.lean

added theorem invOf_lt_one

Modified Mathlib/Analysis/Convex/Segment.lean

added theorem mem_openSegment_add_sub

added theorem mem_openSegment_sub_add

modified theorem mem_segment_add_sub

modified theorem mem_segment_sub_add

added theorem midpoint_mem_openSegment

modified theorem midpoint_mem_segment