Commit 2024-09-30 15:50 656765e9

View on Github →

feat(MetricSpace/Ultra): TotallyDisconnectedSpace X when X is ultrametric (#17297)

Estimated changes

Modified Mathlib.lean

Created Mathlib/Topology/MetricSpace/Ultra/TotallyDisconnected.lean