Commit 2024-10-31 06:53 ee376587

View on Github →

chore: cleanup ContDiffWithinAt API, to match the ContinuousAt API (#18447) Follow up to #17927. We make sure that the API for ContDiffWithinAt matches the one for ContinuousAt, adding a bunch of missing lemmas and renaming a few of them. Notably

  • ContinuousAt.continuousOn becomes continuousOn_of_forall_continuousAt (as there is a lemma ContDiffAt.contDiffOn with a completely different meaning)
  • Use assumptions MapsTo f s t instead of s ⊆ f ⁻¹' t in several statements
  • Add of_eq versions of all composition lemmas for ContDiff-type statements
  • Rename ContDiff.comp_contDiffOn₂ to ContDiff.comp₂_contDiffOn, to follow the convention in Continuous lemmas
  • Rename ContDiffWithinAt.mono_of_mem to ContDiffWithinAt.mono_of_mem_nhdsWithin to clarify what the lemma does
  • Change from ContDiffWithinAt.congr_nhds, taking an assumption 𝓝[s] x = 𝓝[t] x, to ContDiffWithinAt.congr_set, taking an assumption s =ᶠ[𝓝 x] t. I have added deprecations to all lemmas with changed names.

Estimated changes

modified theorem ContDiff.clm_apply
modified theorem ContDiff.smulRight
added theorem ContDiffAt.clm_apply
added theorem ContDiffAt.clm_comp
added theorem ContDiffAt.comp₂
added theorem ContDiffAt.smulRight
modified theorem ContDiffOn.clm_apply
deleted theorem ContDiffOn.comp'
added theorem ContDiffOn.comp_inter
added theorem ContDiffOn.smulRight
added theorem IsOpen.contDiffOn_iff
added theorem contDiffWithinAt_congr
modified theorem Set.MapsTo.subset_preimage
deleted theorem ContinuousAt.continuousOn