Theorem right_mem_openSegment_iff

Modification history

2026-01-13 19:40

Mathlib/Analysis/Convex/Segment.lean

chore(Algebra): replace `NoZeroSMulDivisors` with `Module.IsTorsionFree` wlog (#30563) …

Modified right_mem_openSegment_iff View on Github →

2023-03-24 15:22

Mathlib/Analysis/Convex/Segment.lean

feat: port Analysis.Convex.Segment (#2869)

Added right_mem_openSegment_iff View on Github →