Theorem MeasureTheory.eventuallyEmptyOrUniv_smul_set_ae

Modification history

2026-09-03 20:16
Mathlib/MeasureTheory/Group/Action.lean
refactor: definition for `EventuallyConst` on `Set` (#43114) …
Added MeasureTheory.eventuallyEmptyOrUniv_smul_set_aeView on Github →