Commit 2024-08-31 14:29 b5690dbd

View on Github →

chore: Namespace UniformSpace.ball API (#16113) All these lemmas have pretty generic names

Estimated changes

modified def UniformSpace.ball
added theorem UniformSpace.ball_mono
modified theorem UniformSpace.isClosed_ball
modified theorem UniformSpace.isOpen_ball
modified theorem UniformSpace.mem_ball_self
deleted theorem ball_eq_of_symmetry
deleted theorem ball_inter
deleted theorem ball_inter_left
deleted theorem ball_inter_right
deleted theorem ball_mono
deleted theorem mem_ball_comp
deleted theorem mem_ball_symmetry
deleted theorem mem_comp_comp
deleted theorem mem_comp_of_mem_ball