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.



Co-authored-by: Junyan Xu <junyanxu.math@gmail.com>

Mathlib/Dynamics/Flow.lean

@@ -137,7 +137,7 @@ theorem map_zero_apply (x : α) : ϕ 0 x = x := ϕ.map_zero' x
     to itself defines a semiflow by `ℕ` on `α`. -/
 def fromIter {g : α → α} (h : Continuous g) : Flow ℕ α where
   toFun n x := g^[n] x
-  cont' := continuous_uncurry_of_discreteTopology_left (Continuous.iterate h)
+  cont' := continuous_prod_of_discrete_left.mpr (Continuous.iterate h)
   map_add' := iterate_add_apply _
   map_zero' _x := rfl
 #align flow.from_iter Flow.fromIter

Mathlib/Topology/Algebra/Group/Basic.lean

@@ -499,7 +499,7 @@ instance AddGroup.continuousConstSMul_int {A} [AddGroup A] [TopologicalSpace A]
 
 instance AddGroup.continuousSMul_int {A} [AddGroup A] [TopologicalSpace A]
     [TopologicalAddGroup A] : ContinuousSMul ℤ A :=
-  ⟨continuous_uncurry_of_discreteTopology continuous_zsmul⟩
+  ⟨continuous_prod_of_discrete_left.mpr continuous_zsmul⟩
 #align add_group.has_continuous_smul_int AddGroup.continuousSMul_int
 
 @[to_additive (attr := continuity)]

Mathlib/Topology/Algebra/Monoid.lean

@@ -570,7 +570,7 @@ instance AddMonoid.continuousConstSMul_nat {A} [AddMonoid A] [TopologicalSpace A
 
 instance AddMonoid.continuousSMul_nat {A} [AddMonoid A] [TopologicalSpace A]
     [ContinuousAdd A] : ContinuousSMul ℕ A :=
-  ⟨continuous_uncurry_of_discreteTopology continuous_nsmul⟩
+  ⟨continuous_prod_of_discrete_left.mpr continuous_nsmul⟩
 #align add_monoid.has_continuous_smul_nat AddMonoid.continuousSMul_nat
 
 @[to_additive (attr := continuity)]

Mathlib/Topology/Constructions.lean

@@ -522,16 +522,7 @@ theorem nhdsWithin_prod_eq (a : α) (b : β) (s : Set α) (t : Set β) :
   simp only [nhdsWithin, nhds_prod_eq, ← prod_inf_prod, prod_principal_principal]
 #align nhds_within_prod_eq nhdsWithin_prod_eq
 
-/-- If a function `f x y` is such that `y ↦ f x y` is continuous for all `x`, and `x` lives in a
-discrete space, then `f` is continuous. -/
-theorem continuous_uncurry_of_discreteTopology [DiscreteTopology α] {f : α → β → γ}
-    (hf : ∀ a, Continuous (f a)) : Continuous (uncurry f) := by
-  apply continuous_iff_continuousAt.2
-  rintro ⟨a, x⟩
-  change map _ _ ≤ _
-  rw [nhds_prod_eq, nhds_discrete, Filter.map_pure_prod]
-  exact (hf a).continuousAt
-#align continuous_uncurry_of_discrete_topology continuous_uncurry_of_discreteTopology
+#noalign continuous_uncurry_of_discrete_topology
 
 theorem mem_nhds_prod_iff {a : α} {b : β} {s : Set (α × β)} :
     s ∈ 𝓝 (a, b) ↔ ∃ u ∈ 𝓝 a, ∃ v ∈ 𝓝 b, u ×ˢ v ⊆ s := by rw [nhds_prod_eq, mem_prod_iff]
@@ -676,12 +667,7 @@ theorem prod_induced_induced (f : α → β) (g : γ → δ) :
   rfl
 #align prod_induced_induced prod_induced_induced
 
-theorem continuous_uncurry_of_discreteTopology_left [DiscreteTopology α] {f : α → β → γ}
-    (h : ∀ a, Continuous (f a)) : Continuous (uncurry f) :=
-  continuous_iff_continuousAt.2 fun ⟨a, b⟩ => by
-    simp only [ContinuousAt, nhds_prod_eq, nhds_discrete α, pure_prod, tendsto_map'_iff, (· ∘ ·),
-      uncurry, (h a).tendsto]
-#align continuous_uncurry_of_discrete_topology_left continuous_uncurry_of_discreteTopology_left
+#noalign continuous_uncurry_of_discrete_topology_left
 
 /-- Given a neighborhood `s` of `(x, x)`, then `(x, x)` has a square open neighborhood
   that is a subset of `s`. -/

Mathlib/Topology/ContinuousOn.lean

@@ -543,6 +543,11 @@ theorem continuousWithinAt_univ (f : α → β) (x : α) :
   rw [ContinuousAt, ContinuousWithinAt, nhdsWithin_univ]
 #align continuous_within_at_univ continuousWithinAt_univ
 
+theorem continuous_iff_continuousOn_univ {f : α → β} : Continuous f ↔ ContinuousOn f univ := by
+  simp [continuous_iff_continuousAt, ContinuousOn, ContinuousAt, ContinuousWithinAt,
+    nhdsWithin_univ]
+#align continuous_iff_continuous_on_univ continuous_iff_continuousOn_univ
+
 theorem continuousWithinAt_iff_continuousAt_restrict (f : α → β) {x : α} {s : Set α} (h : x ∈ s) :
     ContinuousWithinAt f s x ↔ ContinuousAt (s.restrict f) ⟨x, h⟩ :=
   tendsto_nhdsWithin_iff_subtype h f _
@@ -566,6 +571,44 @@ theorem ContinuousWithinAt.prod_map {f : α → γ} {g : β → δ} {s : Set α}
   exact hf.prod_map hg
 #align continuous_within_at.prod_map ContinuousWithinAt.prod_map
 
+theorem continuousWithinAt_prod_of_discrete_left [DiscreteTopology α]
+    {f : α × β → γ} {s : Set (α × β)} {x : α × β} :
+    ContinuousWithinAt f s x ↔ ContinuousWithinAt (f ⟨x.1, ·⟩) {b | (x.1, b) ∈ s} x.2 := by
+  rw [← x.eta]; simp_rw [ContinuousWithinAt, nhdsWithin, nhds_prod_eq, nhds_discrete, pure_prod,
+    ← map_inf_principal_preimage]; rfl
+
+theorem continuousWithinAt_prod_of_discrete_right [DiscreteTopology β]
+    {f : α × β → γ} {s : Set (α × β)} {x : α × β} :
+    ContinuousWithinAt f s x ↔ ContinuousWithinAt (f ⟨·, x.2⟩) {a | (a, x.2) ∈ s} x.1 := by
+  rw [← x.eta]; simp_rw [ContinuousWithinAt, nhdsWithin, nhds_prod_eq, nhds_discrete, prod_pure,
+    ← map_inf_principal_preimage]; rfl
+
+theorem continuousAt_prod_of_discrete_left [DiscreteTopology α] {f : α × β → γ} {x : α × β} :
+    ContinuousAt f x ↔ ContinuousAt (f ⟨x.1, ·⟩) x.2 := by
+  simp_rw [← continuousWithinAt_univ]; exact continuousWithinAt_prod_of_discrete_left
+
+theorem continuousAt_prod_of_discrete_right [DiscreteTopology β] {f : α × β → γ} {x : α × β} :
+    ContinuousAt f x ↔ ContinuousAt (f ⟨·, x.2⟩) x.1 := by
+  simp_rw [← continuousWithinAt_univ]; exact continuousWithinAt_prod_of_discrete_right
+
+theorem continuousOn_prod_of_discrete_left [DiscreteTopology α] {f : α × β → γ} {s : Set (α × β)} :
+    ContinuousOn f s ↔ ∀ a, ContinuousOn (f ⟨a, ·⟩) {b | (a, b) ∈ s} := by
+  simp_rw [ContinuousOn, Prod.forall, continuousWithinAt_prod_of_discrete_left]; rfl
+
+theorem continuousOn_prod_of_discrete_right [DiscreteTopology β] {f : α × β → γ} {s : Set (α × β)} :
+    ContinuousOn f s ↔ ∀ b, ContinuousOn (f ⟨·, b⟩) {a | (a, b) ∈ s} := by
+  simp_rw [ContinuousOn, Prod.forall, continuousWithinAt_prod_of_discrete_right]; apply forall_swap
+
+/-- If a function `f a b` is such that `y ↦ f a b` is continuous for all `a`, and `a` lives in a
+discrete space, then `f` is continuous, and vice versa. -/
+theorem continuous_prod_of_discrete_left [DiscreteTopology α] {f : α × β → γ} :
+    Continuous f ↔ ∀ a, Continuous (f ⟨a, ·⟩) := by
+  simp_rw [continuous_iff_continuousOn_univ]; exact continuousOn_prod_of_discrete_left
+
+theorem continuous_prod_of_discrete_right [DiscreteTopology β] {f : α × β → γ} :
+    Continuous f ↔ ∀ b, Continuous (f ⟨·, b⟩) := by
+  simp_rw [continuous_iff_continuousOn_univ]; exact continuousOn_prod_of_discrete_right
+
 theorem continuousWithinAt_pi {ι : Type*} {π : ι → Type*} [∀ i, TopologicalSpace (π i)]
     {f : α → ∀ i, π i} {s : Set α} {x : α} :
     ContinuousWithinAt f s x ↔ ∀ i, ContinuousWithinAt (fun y => f y i) s x :=
@@ -687,11 +730,6 @@ theorem comap_nhdsWithin_range {α} (f : α → β) (y : β) : comap f (𝓝[ran
   comap_inf_principal_range
 #align comap_nhds_within_range comap_nhdsWithin_range
 
-theorem continuous_iff_continuousOn_univ {f : α → β} : Continuous f ↔ ContinuousOn f univ := by
-  simp [continuous_iff_continuousAt, ContinuousOn, ContinuousAt, ContinuousWithinAt,
-    nhdsWithin_univ]
-#align continuous_iff_continuous_on_univ continuous_iff_continuousOn_univ
-
 theorem ContinuousWithinAt.mono {f : α → β} {s t : Set α} {x : α} (h : ContinuousWithinAt f t x)
     (hs : s ⊆ t) : ContinuousWithinAt f s x :=
   h.mono_left (nhdsWithin_mono x hs)