Theorems · Theorem · general topology

uniformity_basis_edist

∀ {α : Type u} [inst : PseudoEMetricSpace α], (uniformity α).HasBasis (fun ε => 0 < ε) fun ε => {p | edist p.1 p.2 < ε}

Defined in

Mathlib.Topology.EMetricSpace.Defs

Cited by

17 results in Mathlib

Foundations

Depth 139 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

PseudoEMetricSpace