Commit 2024-02-06 07:03 d78efd06

View on Github →

chore(NormedSpace/Basic): move some theorems to NormedSpace.Real (#10206) This way we don't switch between general normed spaces and real normed spaces back and forth throughout the file.

Estimated changes

deleted theorem closure_ball
deleted theorem exists_norm_eq
deleted theorem frontier_ball
deleted theorem frontier_closedBall'
deleted theorem frontier_closedBall
deleted theorem frontier_sphere'
deleted theorem frontier_sphere
deleted theorem interior_closedBall'
deleted theorem interior_closedBall
deleted theorem interior_sphere'
deleted theorem interior_sphere
deleted theorem nnnorm_surjective
deleted theorem norm_smul_of_nonneg
deleted theorem range_nnnorm
deleted theorem range_norm
added theorem closure_ball
added theorem exists_norm_eq
added theorem frontier_ball
added theorem frontier_closedBall'
added theorem frontier_closedBall
added theorem frontier_sphere'
added theorem frontier_sphere
added theorem interior_closedBall'
added theorem interior_closedBall
added theorem interior_sphere'
added theorem interior_sphere
added theorem nnnorm_surjective
added theorem norm_smul_of_nonneg
added theorem range_nnnorm
added theorem range_norm