Commit 2024-02-17 16:56 996ae393

View on Github →

chore(Topology): Inhabited -> Nonempty (#10647)

Estimated changes

Modified Mathlib/Topology/MetricSpace/GromovHausdorffRealized.lean

modified def GromovHausdorff.candidatesBDist

Modified Mathlib/Topology/Sheaves/SheafCondition/OpensLeCover.lean