Commit 2025-03-17 13:56 37315603

View on Github →

chore(Filter,Topology): add simple lemmas (#22720)

Add Filter.NeBot ⊤
Add Filter.Frequently.of_curry.
Add a few lemmas about MapClusterPt

Estimated changes

Modified Mathlib/Dynamics/OmegaLimit.lean

Modified Mathlib/MeasureTheory/Measure/EverywherePos.lean

Modified Mathlib/Order/Filter/Basic.lean

Modified Mathlib/Order/Filter/Prod.lean

added theorem Filter.Frequently.of_curry

Modified Mathlib/Topology/Algebra/InfiniteSum/Constructions.lean

Modified Mathlib/Topology/Basic.lean

added theorem ClusterPt.frequently

added theorem Filter.EventuallyEq.mapClusterPt_iff

added theorem MapClusterPt.frequently

deleted theorem clusterPt_iff

added theorem clusterPt_iff_frequently

added theorem clusterPt_iff_nonempty

deleted theorem mapClusterPt_iff

added theorem mapClusterPt_iff_frequently

Modified Mathlib/Topology/Compactness/Compact.lean

Modified Mathlib/Topology/Compactness/Lindelof.lean

Modified Mathlib/Topology/Constructions.lean

Modified Mathlib/Topology/UniformSpace/OfCompactT2.lean