Theorem TopologicalSpace.NonemptyCompacts.dist_eq

Modification history

2026-09-09 04:05
Mathlib/Topology/MetricSpace/Closeds.lean
chore(Topology/MetricSpace/Closeds): rename lemmas about `MetricSpace (NonemptyCompacts α)` (#42774) …
Added TopologicalSpace.NonemptyCompacts.dist_eqView on Github →