Commit 2024-10-30 09:35 93eaeab2

View on Github โ†’

chore: uniformize ContDiffWithinAt API with other local notions (#17927) Currently, some statements are available for DifferentiableWithinAt but not for ContinuousWithinAt or conversely (and the same for the other WithinAt notions), or they are both available with slightly different names or assumptions. This PR is a first step to uniformize these API: I've gone through the APIs of the different notions, and added all the lemmas that were available for another notion to ContinuousWithinAt if they were missing here, and fixed some names. Once this PR is merged, I will open other PRs to make sure that all the other notions also have the same full API. Notable changes (imported from lemma names of other notions, and that I found better than the ContinuousWithinAt version):

  • rename ContinuousWithinAt.insert_self to ContinuousWithinAt.insert
  • rename continuousWithinAt_congr_nhds to continuousWithinAt_congr_set, and change its assumptions from ๐“[s] x = ๐“[t] x to s =แถ [๐“ x] t (see Zulip discussion supporting this change at https://leanprover.zulipchat.com/#narrow/channel/287929-mathlib4/topic/local.20equality.20of.20sets/near/477653314)
  • Added continuousWithinAt_congr_set' (taking an assumption s =แถ [๐“[{y}แถœ] x] t)
  • Added several variations around ContinuousWithinAt.congr_of_mem (both in their implication and iff version)
  • Added of_eq versions of all the composition lemmas Also, use variable in the ContinuousOn file.

Estimated changes

deleted theorem ContDiffWithinAt.comp'
deleted theorem ContDiffWithinAt.congr'
modified theorem Continuous.continuousOn
modified theorem Continuous.if
modified theorem Continuous.if_const
modified theorem Continuous.piecewise
modified theorem ContinuousAt.continuousOn
deleted theorem ContinuousOn.comp''
modified theorem ContinuousOn.comp
modified theorem ContinuousOn.congr
modified theorem ContinuousOn.congr_mono
modified theorem ContinuousOn.continuousAt
modified theorem ContinuousOn.if
modified theorem ContinuousOn.image_closure
modified theorem ContinuousOn.mono
modified theorem ContinuousOn.piecewise'
modified theorem ContinuousOn.piecewise
deleted theorem ContinuousWithinAt.comp'
modified theorem ContinuousWithinAt.comp
modified theorem ContinuousWithinAt.congr
modified theorem ContinuousWithinAt.diff_iff
modified theorem ContinuousWithinAt.mono
modified theorem ContinuousWithinAt.tendsto
modified theorem ContinuousWithinAt.union
modified theorem IsOpen.continuousOn_iff
modified theorem IsOpen.ite'
modified theorem IsOpen.ite
modified theorem continuousAt_update_same
modified theorem continuousOn_congr
modified theorem continuousOn_iff'
modified theorem continuousOn_iff
modified theorem continuousOn_iff_isClosed
modified theorem continuousOn_open_iff
modified theorem continuousOn_piecewise_ite'
modified theorem continuousOn_piecewise_ite
modified theorem continuousWithinAt_inter'
modified theorem continuousWithinAt_inter
modified theorem continuousWithinAt_union
modified theorem continuous_if'
modified theorem continuous_if
modified theorem continuous_if_const
modified theorem continuous_of_cover_nhds
modified theorem continuous_piecewise
modified theorem nhdsWithin_le_comap
added theorem eventuallyEq_insert