Commit 2023-09-04 12:27 699bc905

View on Github →

chore(Analysis): rename lipschitz_on_univ to lipschitzOn_univ (#6946) Also rename dimH_image_le_of_locally_lipschitz_on to dimH_image_le_of_locally_lipschitzOn.

Estimated changes

Modified Mathlib/Analysis/Calculus/FDeriv/Basic.lean

Modified Mathlib/Analysis/Calculus/Inverse.lean

Modified Mathlib/Analysis/Calculus/MeanValue.lean

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

added theorem IsCompact.exists_bound_of_continuousOn'

deleted theorem IsCompact.exists_bound_of_continuous_on'

Modified Mathlib/Analysis/NormedSpace/lpSpace.lean

Modified Mathlib/Topology/Algebra/Polynomial.lean

Modified Mathlib/Topology/Instances/ENNReal.lean

Modified Mathlib/Topology/MetricSpace/HausdorffDimension.lean

added theorem dimH_image_le_of_locally_lipschitzOn

deleted theorem dimH_image_le_of_locally_lipschitz_on

added theorem dimH_range_le_of_locally_lipschitzOn

deleted theorem dimH_range_le_of_locally_lipschitz_on

Modified Mathlib/Topology/MetricSpace/Holder.lean

Modified Mathlib/Topology/MetricSpace/Lipschitz.lean

added theorem lipschitzOn_univ

deleted theorem lipschitz_on_univ