Theorem UniformSpace.Core.nhds_toTopologicalSpace

Modification history

2025-02-10 19:51

Mathlib/Topology/UniformSpace/Basic.lean

chore(Topology/UniformSpace): split into `Defs` and `Basic` (#21664) …

Modified UniformSpace.Core.nhds_toTopologicalSpace View on Github →

2024-03-20 13:11

Mathlib/Topology/UniformSpace/Basic.lean

refactor(UniformSpace): change the definition (#10901) …

Added UniformSpace.Core.nhds_toTopologicalSpace View on Github →