Theorem UniformSpace.isClosed_ball

Modification history

2024-08-31 14:29

Mathlib/Topology/UniformSpace/Basic.lean

chore: Namespace `UniformSpace.ball` API (#16113) …

Modified UniformSpace.isClosed_ball View on Github →

2024-02-21 15:14

Mathlib/Topology/UniformSpace/Basic.lean

feat(UniformSpace): add `UniformSpace.isClosed_ball` (#10782)

Added UniformSpace.isClosed_ball View on Github →