Theorem measurableSet_eq_fun'

Modification history

2025-01-16 10:00
Mathlib/MeasureTheory/Group/Arithmetic.lean
refactor: make `CanonicallyOrdered...` mixin (#17444) …
Modified measurableSet_eq_fun'View on Github →
2024-03-13 15:40
Mathlib/MeasureTheory/Group/Arithmetic.lean
feat: add a variant of `measurableSet_eq_fun` that applies to ENNReal (#11275)
Added measurableSet_eq_fun'View on Github →