TotallySeparated

📁 Source: Mathlib/Topology/MetricSpace/Ultra/TotallySeparated.lean

Statistics

Metric	Count
Definitions	0
Theorems instTotallySeparatedSpaceOfIsUltrametricDist	1
Total	1

(root)

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
instTotallySeparatedSpaceOfIsUltrametricDist 📖	mathematical	—	TotallySeparatedSpace UniformSpace.toTopologicalSpace PseudoMetricSpace.toUniformSpace MetricSpace.toPseudoMetricSpace	—	totallySeparatedSpace_iff_exists_isClopen exists_between LinearOrderedSemiField.toDenselyOrdered PosMulReflectLE.toPosMulReflectLT PosMulStrictMono.toPosMulReflectLE IsStrictOrderedRing.toPosMulStrictMono Real.instIsStrictOrderedRing dist_pos IsUltrametricDist.isClopen_ball dist_self dist_comm LT.lt.le

---

← Back to Index