Commit 2024-07-20 18:20 2474112e

View on Github →

feat(MeasureTheory/Group): add lemmas about Filter.EventuallyConst (#14595) Add MeasureTheory.eventuallyConst_smul_set_ae and MeasureTheory.eventuallyConst_inv_set_ae.

Estimated changes

Modified Mathlib/MeasureTheory/Group/Action.lean

added theorem MeasureTheory.eventuallyConst_smul_set_ae

Modified Mathlib/MeasureTheory/Group/Prod.lean

added theorem MeasureTheory.eventuallyConst_inv_set_ae

Modified Mathlib/Order/Filter/EventuallyConst.lean

added theorem Filter.eventuallyConst_preimage