Commit 2025-04-07 16:11 8fa3d6b6

View on Github →

chore: split IsTopologicalBasis results out of Compactness.Compact (#23401) Copyright from: https://github.com/leanprover-community/mathlib3/pull/15436 and https://github.com/leanprover-community/mathlib4/pull/12986.

Estimated changes

Modified Mathlib.lean

Modified Mathlib/Topology/ClopenBox.lean

Created Mathlib/Topology/Compactness/Bases.lean

added theorem eq_finite_iUnion_of_isTopologicalBasis_of_isCompact_open

added theorem eq_sUnion_finset_of_isTopologicalBasis_of_isCompact_open

added theorem isCompact_open_iff_eq_finite_iUnion_of_isTopologicalBasis

Modified Mathlib/Topology/Compactness/Compact.lean

deleted theorem eq_finite_iUnion_of_isTopologicalBasis_of_isCompact_open

deleted theorem eq_sUnion_finset_of_isTopologicalBasis_of_isCompact_open

deleted theorem isCompact_open_iff_eq_finite_iUnion_of_isTopologicalBasis

Modified Mathlib/Topology/Compactness/SigmaCompact.lean

Modified Mathlib/Topology/Constructible.lean

Modified Mathlib/Topology/QuasiSeparated.lean

Modified Mathlib/Topology/Separation/Basic.lean

Modified Mathlib/Topology/Sets/Opens.lean