From 87eb696ebcebeb067820a70014c6e31c1fe54cb2 Mon Sep 17 00:00:00 2001 From: Junyan Xu Date: Thu, 5 Oct 2023 13:18:23 +0000 Subject: [PATCH] feat(Topology): continuity from a product with a discrete space (#7511) MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit + 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 --- Mathlib/Dynamics/Flow.lean | 2 +- Mathlib/Topology/Algebra/Group/Basic.lean | 2 +- Mathlib/Topology/Algebra/Monoid.lean | 2 +- Mathlib/Topology/Constructions.lean | 18 +-------- Mathlib/Topology/ContinuousOn.lean | 48 ++++++++++++++++++++--- 5 files changed, 48 insertions(+), 24 deletions(-) diff --git a/Mathlib/Dynamics/Flow.lean b/Mathlib/Dynamics/Flow.lean index 0508f9e7eb9a5..ff109a643da99 100644 --- a/Mathlib/Dynamics/Flow.lean +++ b/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 diff --git a/Mathlib/Topology/Algebra/Group/Basic.lean b/Mathlib/Topology/Algebra/Group/Basic.lean index 5a60759084e14..323e6e867034c 100644 --- a/Mathlib/Topology/Algebra/Group/Basic.lean +++ b/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)] diff --git a/Mathlib/Topology/Algebra/Monoid.lean b/Mathlib/Topology/Algebra/Monoid.lean index 58071f271eaba..3588d544d643b 100644 --- a/Mathlib/Topology/Algebra/Monoid.lean +++ b/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)] diff --git a/Mathlib/Topology/Constructions.lean b/Mathlib/Topology/Constructions.lean index 202e0e84a3000..ffba5130508e1 100644 --- a/Mathlib/Topology/Constructions.lean +++ b/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`. -/ diff --git a/Mathlib/Topology/ContinuousOn.lean b/Mathlib/Topology/ContinuousOn.lean index 9df3f81637a03..4d3ed90b09d3d 100644 --- a/Mathlib/Topology/ContinuousOn.lean +++ b/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)