Commit 2023-10-05 13:18 87eb696e

View on Github →

feat(Topology): continuity from a product with a discrete space (#7511)

Add four pairs of lemmas continuous((Within)At/On)_prod_of_discrete_left/right in ContinuousOn.lean: to check continuity of a function from X × Y to Z with X discrete, it suffices to check continuity of every slice of it with x : X fixed.
Remove duplicate lemmas continuous_uncurry_of_discreteTopology(_left) from Constructions.lean in favor of the more general (iff) version.
Move the lemma continuous_iff_continuousOn_univ up.

Estimated changes

Modified Mathlib/Dynamics/Flow.lean

Modified Mathlib/Topology/Algebra/Group/Basic.lean

Modified Mathlib/Topology/Algebra/Monoid.lean

Modified Mathlib/Topology/Constructions.lean

deleted theorem continuous_uncurry_of_discreteTopology

deleted theorem continuous_uncurry_of_discreteTopology_left

Modified Mathlib/Topology/ContinuousOn.lean

added theorem continuousAt_prod_of_discrete_left

added theorem continuousAt_prod_of_discrete_right

added theorem continuousOn_prod_of_discrete_left

added theorem continuousOn_prod_of_discrete_right

added theorem continuousWithinAt_prod_of_discrete_left

added theorem continuousWithinAt_prod_of_discrete_right

added theorem continuous_prod_of_discrete_left

added theorem continuous_prod_of_discrete_right