Theorem TopologicalSpace.Compacts.disjoint_coe_iff

Modification history

2026-07-12 20:38
Mathlib/Topology/Sets/Compacts.lean
feat(Topology/Sets): disjoint `Compacts` form an open set (#40053)
Added TopologicalSpace.Compacts.disjoint_coe_iffView on Github →