Commit 2024-12-18 13:02 79dae4b2

View on Github →

chore(Analysis): rename closedUnitBall and closed_unit_ball to unitClosedBall (#9755) Since closedBall is a function name, it should appear as an unbroken token in the lemma name Zulip poll

Estimated changes

Modified Mathlib/Analysis/BoxIntegral/Basic.lean

Modified Mathlib/Analysis/CStarAlgebra/Multiplier.lean

Modified Mathlib/Analysis/CStarAlgebra/Unitization.lean

Modified Mathlib/Analysis/Convex/StrictConvexSpace.lean

deleted theorem StrictConvexSpace.of_strictConvex_closed_unit_ball

added theorem StrictConvexSpace.of_strictConvex_unitClosedBall

Modified Mathlib/Analysis/Normed/Field/Basic.lean

deleted theorem NormedDivisionRing.discreteTopology_unit_closedBall_eq_univ

added theorem NormedDivisionRing.unitClosedBall_eq_univ_of_discrete

Modified Mathlib/Analysis/Normed/Field/Lemmas.lean

Modified Mathlib/Analysis/NormedSpace/OperatorNorm/NNNorm.lean

deleted theorem ContinuousLinearMap.sSup_closed_unit_ball_eq_nnnorm

deleted theorem ContinuousLinearMap.sSup_closed_unit_ball_eq_norm

added theorem ContinuousLinearMap.sSup_unitClosedBall_eq_nnnorm

added theorem ContinuousLinearMap.sSup_unitClosedBall_eq_norm

Modified Mathlib/Analysis/NormedSpace/Pointwise.lean

deleted theorem smul_closedUnitBall

deleted theorem smul_closedUnitBall_of_nonneg

added theorem smul_unitClosedBall

added theorem smul_unitClosedBall_of_nonneg

Modified Mathlib/Analysis/NormedSpace/Real.lean

deleted theorem inv_norm_smul_mem_closed_unit_ball

added theorem inv_norm_smul_mem_unitClosedBall

Modified Mathlib/MeasureTheory/Measure/Lebesgue/EqHaar.lean

deleted theorem MeasureTheory.Measure.addHaar_closed_unit_ball_eq_addHaar_unit_ball

added theorem MeasureTheory.Measure.addHaar_unitClosedBall_eq_addHaar_unitBall