Ultrametric spaces are totally separated #
In a metric space with an ultrametric, the space is totally separated, hence totally disconnected.
Tags #
ultrametric, nonarchimedean, totally separated, totally disconnected
instance
instTotallySeparatedSpaceOfIsUltrametricDist
{X : Type u_1}
[MetricSpace X]
[IsUltrametricDist X]
:
Equations
- ⋯ = ⋯