Commit 2025-12-05 17:27 5a54f93b

View on Github →

chore: remove finiteness from Order.Filter.Lift (#23411)

Estimated changes

Modified Mathlib/Dynamics/TopologicalEntropy/DynamicalEntourage.lean

Modified Mathlib/Order/Filter/Basic.lean

added theorem Filter.iInf_sets_induct

Modified Mathlib/Order/Filter/Finite.lean

deleted theorem Filter.iInf_sets_induct

Modified Mathlib/Order/Filter/Lift.lean

Modified Mathlib/Order/Filter/SmallSets.lean

Modified Mathlib/Topology/Algebra/ContinuousMonoidHom.lean

Modified Mathlib/Topology/Algebra/Monoid/Defs.lean