Theorem Set.Ioc_eq_Ioc_iff

Modification history

2026-01-27 08:06
Mathlib/Order/Interval/Set/LinearOrder.lean
feat: additive content on open-closed intervals, mapping `(u, v]` to `f v - f u` (#34462) …
Added Set.Ioc_eq_Ioc_iffView on Github →