[Merged by Bors] - chore(Analysis): rename `closedUnitBall` and `closed_unit_ball` to `unitClosedBall`#9755

Closed

eric-wieser wants to merge 4 commits intomasterfrom eric-wieser/rename-closedBall-lemmas

+53-29

Commits on Dec 1, 2024

chore(Analysis): rename closedUnitBall and closed_unit_ball to unit_closedBall

eric-wieser
authored and
YaelDillies
committed
deprecated aliases
YaelDillies
committed

Commits on Dec 2, 2024

rename to unitClosedBall_eq_univ_of_discrete
YaelDillies
committed

Commits on Dec 18, 2024

rename once more
YaelDillies
committed