Commit 2026-10-28 22:35 1d11fcd1

View on Github →

chore(Topology): deprecate UniformSpace.ball in favor of SetRel.ball (#44887) Since UniformSpace.ball is a right-ball and SetRel.ball is a left-ball, we need to move around some appeals to symmetry of the relation. Follow-up to #33077.

Estimated changes

modified theorem UniformSpace.isClosed_ball
modified theorem UniformSpace.isOpen_ball
modified theorem closure_ball_subset
added theorem SetRel.ball_mem_nhds
modified theorem UniformSpace.ball_mem_nhds
modified theorem UniformSpace.mem_nhds_iff
modified theorem isOpen_iff_ball_subset
modified theorem mem_nhds_left
modified theorem nhds_eq_uniformity'
modified theorem nhds_eq_uniformity
modified theorem ball_eq_of_mem
modified theorem ball_subset_of_mem