Commit 2024-11-02 01:04 f7f18c5d

View on Github →

chore: delay importing ultrafilters (#18328) Delays import Ultrafilters, which currently bring in quite a few unnecessary imports into basic topology. Three proofs broke, which Patrick has replaced with essentially logically identical proofs, but which don't mention ultrafilters.

Estimated changes

Modified Mathlib.lean

Modified Mathlib/Topology/Basic.lean

deleted theorem Ultrafilter.clusterPt_iff

deleted theorem clusterPt_iff_ultrafilter

deleted theorem continuousAt_iff_ultrafilter

deleted theorem continuous_iff_ultrafilter

deleted theorem isClosed_iff_ultrafilter

deleted theorem isOpen_iff_ultrafilter

deleted theorem mapClusterPt_iff_ultrafilter

deleted theorem mem_closure_iff_ultrafilter

Modified Mathlib/Topology/Compactness/Compact.lean

Modified Mathlib/Topology/Constructions.lean

Modified Mathlib/Topology/Defs/Filter.lean

Modified Mathlib/Topology/Defs/Sequences.lean

Created Mathlib/Topology/Defs/Ultrafilter.lean

Modified Mathlib/Topology/Inseparable.lean

Modified Mathlib/Topology/Irreducible.lean

Modified Mathlib/Topology/Order.lean

Created Mathlib/Topology/Ultrafilter.lean

added theorem Ultrafilter.clusterPt_iff

added theorem clusterPt_iff_ultrafilter

added theorem continuousAt_iff_ultrafilter

added theorem continuous_iff_ultrafilter

added theorem isClosed_iff_ultrafilter

added theorem isOpen_iff_ultrafilter

added theorem mapClusterPt_iff_ultrafilter

added theorem mem_closure_iff_ultrafilter