Commit 2026-07-12 20:38 f34e7626

View on Github →

feat(Topology/Sets): disjoint Compacts form an open set (#40053)

Estimated changes

Modified Mathlib/Topology/Sets/Compacts.lean

added theorem TopologicalSpace.Compacts.disjoint_coe_iff

Modified Mathlib/Topology/Sets/VietorisTopology.lean

added theorem TopologicalSpace.Compacts.isOpen_setOf_disjoint

added theorem TopologicalSpace.Compacts.isOpen_setOf_disjoint_coe

added theorem TopologicalSpace.NonemptyCompacts.isOpen_setOf_disjoint_coe