Theorem MeasureTheory.eventuallyConst_smul_set_ae

Modification history

2026-09-03 20:16
Mathlib/MeasureTheory/Group/Action.lean
refactor: definition for `EventuallyConst` on `Set` (#43114) …
Deleted MeasureTheory.eventuallyConst_smul_set_aeView on Github →
2024-07-20 18:20
Mathlib/MeasureTheory/Group/Action.lean
feat(MeasureTheory/Group): add lemmas about `Filter.EventuallyConst` (#14595) …
Added MeasureTheory.eventuallyConst_smul_set_aeView on Github →