Theorem UniformSpace.isClosed_ball

Modification history

2025-10-24 14:57
Mathlib/Topology/UniformSpace/Basic.lean
refactor(Topology/UniformSpace): use `SetRel` (#23181) …
Modified UniformSpace.isClosed_ballView on Github →
2024-08-31 14:29
Mathlib/Topology/UniformSpace/Basic.lean
chore: Namespace `UniformSpace.ball` API (#16113) …
Modified UniformSpace.isClosed_ballView on Github →
2024-02-21 15:14
Mathlib/Topology/UniformSpace/Basic.lean
feat(UniformSpace): add `UniformSpace.isClosed_ball` (#10782)
Added UniformSpace.isClosed_ballView on Github →