Commit 2024-03-10 14:17 021eb7a4

View on Github →

feat: Add a few continuity lemmas for products (#10820)

ContinuousAt.comp₂, ContinuousAt.comp₂_continuousWithinAt, and _of_eq versions.
ContinuousAt.along_{fst,snd}: Continuous functions are continuous in their first and second arguments.

Estimated changes

Modified Mathlib/Analysis/Analytic/Constructions.lean

deleted theorem AnalyticAt.along_fst

deleted theorem AnalyticAt.along_snd

added theorem AnalyticAt.curry_left

added theorem AnalyticAt.curry_right

deleted theorem AnalyticOn.along_fst

deleted theorem AnalyticOn.along_snd

added theorem AnalyticOn.curry_left

added theorem AnalyticOn.curry_right

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

Modified Mathlib/Topology/Constructions.lean

added theorem Continuous.curry_left

added theorem Continuous.curry_right

added theorem Continuous.uncurry_left

added theorem Continuous.uncurry_right

added theorem ContinuousAt.comp₂

added theorem ContinuousAt.comp₂_of_eq

deleted theorem continuous_uncurry_left

deleted theorem continuous_uncurry_right

Modified Mathlib/Topology/ContinuousOn.lean

added theorem ContinuousAt.comp₂_continuousWithinAt

added theorem ContinuousAt.comp₂_continuousWithinAt_of_eq

Modified Mathlib/Topology/Separation.lean