Documentation

Mathlib.Topology.MetricSpace.Ultra.TotallyDisconnected

Ultrametric spaces are totally disconnected #

In a metric space with an ultrametric, the space is totally disconnected.

Tags #

ultrametric, nonarchimedean, totally disconnected