Theorem Filter.HasBasis.uniformityPath

Modification history

2025-09-19 12:18

Mathlib/Topology/UniformSpace/Path.lean

feat(Topology/UniformSpace/Path): new file (#24105)

Added Filter.HasBasis.uniformityPath View on Github →