Commit 2024-10-18 09:52 34f08fb6

View on Github →

feat: generalize results from EuclideanSpace to PiLp (#17663) The EuclideanSpace results are left in place for convenience. This generalizes leanprover-community/mathlib3#15363

Estimated changes

added theorem contDiffAt_piLp
added theorem contDiffOn_piLp
added theorem contDiffWithinAt_piLp
added theorem contDiff_piLp
added theorem differentiableAt_piLp
added theorem differentiableOn_piLp
added theorem differentiable_piLp
added theorem hasFDerivWithinAt_piLp
added theorem hasStrictFDerivAt_piLp
modified theorem contDiff_euclidean
modified theorem differentiable_euclidean
deleted def EuclideanSpace.proj
added def PiLp.proj
added def PiLp.projₗ