Commit 2025-04-06 18:39 88042f54

View on Github →

chore: split LocallyFinite results out of Compactness.Compact (#23396) Copyright from: https://github.com/leanprover-community/mathlib3/pull/6352 and https://github.com/leanprover-community/mathlib3/pull/6948.

Estimated changes

Modified Mathlib.lean

Modified Mathlib/Topology/Compactness/Compact.lean

deleted theorem LocallyFinite.finite_nonempty_inter_compact

deleted theorem LocallyFinite.finite_nonempty_of_compact

deleted theorem LocallyFinite.finite_of_compact

Created Mathlib/Topology/Compactness/LocallyFinite.lean

added theorem LocallyFinite.finite_nonempty_inter_compact

added theorem LocallyFinite.finite_nonempty_of_compact

added theorem LocallyFinite.finite_of_compact

Modified Mathlib/Topology/Compactness/SigmaCompact.lean