Commit 2024-10-19 06:27 74600fee

View on Github →

refactor(Order/Filter): don't use generate for CompleteLattice (#17799)

Estimated changes

Modified Mathlib/Analysis/Complex/Basic.lean

Modified Mathlib/Dynamics/Circle/RotationNumber/TranslationNumber.lean

Modified Mathlib/MeasureTheory/Group/Measure.lean

Modified Mathlib/Order/Filter/Basic.lean

deleted theorem Filter.mem_pure

deleted theorem Filter.mem_sSup

added theorem Filter.sets_ssubset_sets

added theorem Filter.sets_subset_sets

Modified Mathlib/Order/Filter/Defs.lean

added theorem Filter.mem_pure

added theorem Filter.mem_sSup