Commit 2025-02-11 13:47 296a9123

View on Github →

chore: isClosed_ball -> isClosed_closedBall (#21709) Surely IsClosed (closedBall _ _) should be named isClosed_closedBall... This has caused some time to be wasted as I was unable to find this lemma with the expected name.

Estimated changes

Modified Mathlib/Analysis/Calculus/InverseFunctionTheorem/ApproximatesLinearOn.lean

Modified Mathlib/Analysis/Convex/Integral.lean

Modified Mathlib/Analysis/Fourier/RiemannLebesgueLemma.lean

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

Modified Mathlib/Analysis/Normed/Module/FiniteDimension.lean

Modified Mathlib/Analysis/NormedSpace/Real.lean

Modified Mathlib/Combinatorics/Additive/AP/Three/Behrend.lean

Modified Mathlib/Geometry/Manifold/BumpFunction.lean

Modified Mathlib/MeasureTheory/Constructions/BorelSpace/Metric.lean

Modified Mathlib/MeasureTheory/Covering/Besicovitch.lean

Modified Mathlib/MeasureTheory/Covering/DensityTheorem.lean

Modified Mathlib/MeasureTheory/Covering/Vitali.lean

Modified Mathlib/MeasureTheory/Function/Jacobian.lean

Modified Mathlib/MeasureTheory/Integral/IntegralEqImproper.lean

Modified Mathlib/MeasureTheory/Integral/PeakFunction.lean

Modified Mathlib/NumberTheory/WellApproximable.lean

Modified Mathlib/Topology/Baire/CompleteMetrizable.lean

Modified Mathlib/Topology/Instances/ENNReal/Lemmas.lean

deleted theorem EMetric.isClosed_ball

added theorem EMetric.isClosed_closedBall

Modified Mathlib/Topology/MetricSpace/Antilipschitz.lean

Modified Mathlib/Topology/MetricSpace/PiNat.lean

Modified Mathlib/Topology/MetricSpace/ProperSpace.lean

Modified Mathlib/Topology/MetricSpace/Pseudo/Lemmas.lean

deleted theorem Metric.isClosed_ball

added theorem Metric.isClosed_closedBall

Modified Mathlib/Topology/MetricSpace/Ultra/Basic.lean