Theorem Path.eqOn_extend_segment

Modification history

2025-10-07 15:26
Mathlib/Analysis/Convex/PathConnected.lean
feat: define `curveIntegral` (#24754) …
Added Path.eqOn_extend_segmentView on Github →