Def TopologicalSpace.PositiveCompacts.toNonemptyCompacts

Modification history

2023-02-14 05:07

Mathlib/Topology/Sets/Compacts.lean

feat: port Topology.Sets.Compacts (#2265)

Added TopologicalSpace.PositiveCompacts.toNonemptyCompacts View on Github →