Theorem SetRel.ball_mem_nhdsWithin

Modification history

2026-10-28 22:35

Mathlib/Topology/UniformSpace/Defs.lean

chore(Topology): deprecate `UniformSpace.ball` in favor of `SetRel.ball` (#44887) …

Added SetRel.ball_mem_nhdsWithin View on Github →