Theorem CurveIntegrable.intervalIntegrable_curveIntegralFun_trans_left

Modification history

2025-10-07 15:26
Mathlib/MeasureTheory/Integral/CurveIntegral/Basic.lean
feat: define `curveIntegral` (#24754) …
Added CurveIntegrable.intervalIntegrable_curveIntegralFun_trans_leftView on Github →