diff --git a/Mathlib/Analysis/LocallyConvex/Barrelled.lean b/Mathlib/Analysis/LocallyConvex/Barrelled.lean index f2f06a246d96a..0fc69ce1805aa 100644 --- a/Mathlib/Analysis/LocallyConvex/Barrelled.lean +++ b/Mathlib/Analysis/LocallyConvex/Barrelled.lean @@ -186,7 +186,7 @@ protected def continuousLinearMapOfTendsto [T2Space F] {l : Filter α} [l.IsCoun rcases l.exists_seq_tendsto with ⟨u, hu⟩ -- We claim that the limit is continuous because it's a limit of an equicontinuous family. -- By the Banach-Steinhaus theorem, this equicontinuity will follow from pointwise boundedness. - refine (h.comp hu).continuous_of_equicontinuousAt (hq.banach_steinhaus ?_).equicontinuous + refine (h.comp hu).continuous_of_equicontinuous (hq.banach_steinhaus ?_).equicontinuous -- For `k` and `x` fixed, we need to show that `(i : ℕ) ↦ q k (g i x)` is bounded. intro k x -- This follows from the fact that this sequences converges (to `q k (f x)`) by hypothesis and diff --git a/Mathlib/Topology/UniformSpace/Equicontinuity.lean b/Mathlib/Topology/UniformSpace/Equicontinuity.lean index ca0adfcbd2b96..e3bb09e8089cd 100644 --- a/Mathlib/Topology/UniformSpace/Equicontinuity.lean +++ b/Mathlib/Topology/UniformSpace/Equicontinuity.lean @@ -33,12 +33,16 @@ For maps between metric spaces, this corresponds to * `Equicontinuous`: equicontinuity of a family of functions on the whole domain * `UniformEquicontinuous`: uniform equicontinuity of a family of functions on the whole domain +We also introduce relative versions, namely `EquicontinuousWithinAt`, `EquicontinuousOn` and +`UniformEquicontinuousOn`, akin to `ContinuousWithinAt`, `ContinuousOn` and `UniformContinuousOn` +respectively. + ## Main statements * `equicontinuous_iff_continuous`: equicontinuity can be expressed as a simple continuity condition between well-chosen function spaces. This is really useful for building up the theory. * `Equicontinuous.closure`: if a set of functions is equicontinuous, its closure - *for the topology of uniform convergence* is also equicontinuous. + *for the topology of pointwise convergence* is also equicontinuous. ## Notations @@ -66,11 +70,6 @@ and `Set.UniformEquicontinuous` asserting the corresponding fact about the famil `(↑) : ↥H → (X → α)` where `H : Set (X → α)`. Note however that these won't work for sets of hom types, and in that case one should go back to the family definition rather than using `Set.image`. -Since we have no use case for it yet, we don't introduce any relative version -(i.e no `EquicontinuousWithinAt` or `EquicontinuousOn`), but this is more of a conservative -position than a design decision, so anyone needing relative versions should feel free to add them, -and that should hopefully be a straightforward task. - ## References * [N. Bourbaki, *General Topology, Chapter X*][bourbaki1966] @@ -83,10 +82,10 @@ equicontinuity, uniform convergence, ascoli section -open UniformSpace Filter Set Uniformity Topology UniformConvergence +open UniformSpace Filter Set Uniformity Topology UniformConvergence Function -variable {ι κ X Y Z α β γ 𝓕 : Type*} [TopologicalSpace X] [TopologicalSpace Y] [TopologicalSpace Z] - [UniformSpace α] [UniformSpace β] [UniformSpace γ] +variable {ι κ X X' Y Z α α' β β' γ 𝓕 : Type*} [tX : TopologicalSpace X] [tY : TopologicalSpace Y] + [tZ : TopologicalSpace Z] [uα : UniformSpace α] [uβ : UniformSpace β] [uγ : UniformSpace γ] /-- A family `F : ι → X → α` of functions from a topological space to a uniform space is *equicontinuous at `x₀ : X`* if, for all entourage `U ∈ 𝓤 α`, there is a neighborhood `V` of `x₀` @@ -101,6 +100,18 @@ protected abbrev Set.EquicontinuousAt (H : Set <| X → α) (x₀ : X) : Prop := EquicontinuousAt ((↑) : H → X → α) x₀ #align set.equicontinuous_at Set.EquicontinuousAt +/-- A family `F : ι → X → α` of functions from a topological space to a uniform space is +*equicontinuous at `x₀ : X` within `S : Set X`* if, for all entourage `U ∈ 𝓤 α`, there is a +neighborhood `V` of `x₀` within `S` such that, for all `x ∈ V` and for all `i : ι`, `F i x` is +`U`-close to `F i x₀`. -/ +def EquicontinuousWithinAt (F : ι → X → α) (S : Set X) (x₀ : X) : Prop := + ∀ U ∈ 𝓤 α, ∀ᶠ x in 𝓝[S] x₀, ∀ i, (F i x₀, F i x) ∈ U + +/-- We say that a set `H : Set (X → α)` of functions is equicontinuous at a point within a subset +if the family `(↑) : ↥H → (X → α)` is equicontinuous at that point within that same subset. -/ +protected abbrev Set.EquicontinuousWithinAt (H : Set <| X → α) (S : Set X) (x₀ : X) : Prop := + EquicontinuousWithinAt ((↑) : H → X → α) S x₀ + /-- A family `F : ι → X → α` of functions from a topological space to a uniform space is *equicontinuous* on all of `X` if it is equicontinuous at each point of `X`. -/ def Equicontinuous (F : ι → X → α) : Prop := @@ -113,9 +124,19 @@ protected abbrev Set.Equicontinuous (H : Set <| X → α) : Prop := Equicontinuous ((↑) : H → X → α) #align set.equicontinuous Set.Equicontinuous +/-- A family `F : ι → X → α` of functions from a topological space to a uniform space is +*equicontinuous on `S : Set X`* if it is equicontinuous *within `S`* at each point of `S`. -/ +def EquicontinuousOn (F : ι → X → α) (S : Set X) : Prop := + ∀ x₀ ∈ S, EquicontinuousWithinAt F S x₀ + +/-- We say that a set `H : Set (X → α)` of functions is equicontinuous on a subset if the family +`(↑) : ↥H → (X → α)` is equicontinuous on that subset. -/ +protected abbrev Set.EquicontinuousOn (H : Set <| X → α) (S : Set X) : Prop := + EquicontinuousOn ((↑) : H → X → α) S + /-- A family `F : ι → β → α` of functions between uniform spaces is *uniformly equicontinuous* if, for all entourage `U ∈ 𝓤 α`, there is an entourage `V ∈ 𝓤 β` such that, whenever `x` and `y` are -`V`-close, we have that, *for all `i : ι`*, `F i x` is `U`-close to `F i x₀`. -/ +`V`-close, we have that, *for all `i : ι`*, `F i x` is `U`-close to `F i y`. -/ def UniformEquicontinuous (F : ι → β → α) : Prop := ∀ U ∈ 𝓤 α, ∀ᶠ xy : β × β in 𝓤 β, ∀ i, (F i xy.1, F i xy.2) ∈ U #align uniform_equicontinuous UniformEquicontinuous @@ -126,6 +147,68 @@ protected abbrev Set.UniformEquicontinuous (H : Set <| β → α) : Prop := UniformEquicontinuous ((↑) : H → β → α) #align set.uniform_equicontinuous Set.UniformEquicontinuous +/-- A family `F : ι → β → α` of functions between uniform spaces is +*uniformly equicontinuous on `S : Set β`* if, for all entourage `U ∈ 𝓤 α`, there is a relative +entourage `V ∈ 𝓤 β ⊓ 𝓟 (S ×ˢ S)` such that, whenever `x` and `y` are `V`-close, we have that, +*for all `i : ι`*, `F i x` is `U`-close to `F i y`. -/ +def UniformEquicontinuousOn (F : ι → β → α) (S : Set β) : Prop := + ∀ U ∈ 𝓤 α, ∀ᶠ xy : β × β in 𝓤 β ⊓ 𝓟 (S ×ˢ S), ∀ i, (F i xy.1, F i xy.2) ∈ U + +/-- We say that a set `H : Set (X → α)` of functions is uniformly equicontinuous on a subset if the +family `(↑) : ↥H → (X → α)` is uniformly equicontinuous on that subset. -/ +protected abbrev Set.UniformEquicontinuousOn (H : Set <| β → α) (S : Set β) : Prop := + UniformEquicontinuousOn ((↑) : H → β → α) S + +lemma EquicontinuousAt.equicontinuousWithinAt {F : ι → X → α} {x₀ : X} (H : EquicontinuousAt F x₀) + (S : Set X) : EquicontinuousWithinAt F S x₀ := + fun U hU ↦ (H U hU).filter_mono inf_le_left + +lemma EquicontinuousWithinAt.mono {F : ι → X → α} {x₀ : X} {S T : Set X} + (H : EquicontinuousWithinAt F T x₀) (hST : S ⊆ T) : EquicontinuousWithinAt F S x₀ := + fun U hU ↦ (H U hU).filter_mono <| nhdsWithin_mono x₀ hST + +@[simp] lemma equicontinuousWithinAt_univ (F : ι → X → α) (x₀ : X) : + EquicontinuousWithinAt F univ x₀ ↔ EquicontinuousAt F x₀ := by + rw [EquicontinuousWithinAt, EquicontinuousAt, nhdsWithin_univ] + +lemma equicontinuousAt_restrict_iff (F : ι → X → α) {S : Set X} (x₀ : S) : + EquicontinuousAt (S.restrict ∘ F) x₀ ↔ EquicontinuousWithinAt F S x₀ := by + simp [EquicontinuousWithinAt, EquicontinuousAt, + ← eventually_nhds_subtype_iff] + +lemma Equicontinuous.equicontinuousOn {F : ι → X → α} (H : Equicontinuous F) + (S : Set X) : EquicontinuousOn F S := + fun x _ ↦ (H x).equicontinuousWithinAt S + +lemma EquicontinuousOn.mono {F : ι → X → α} {S T : Set X} + (H : EquicontinuousOn F T) (hST : S ⊆ T) : EquicontinuousOn F S := + fun x hx ↦ (H x (hST hx)).mono hST + +lemma equicontinuousOn_univ (F : ι → X → α) : + EquicontinuousOn F univ ↔ Equicontinuous F := by + simp [EquicontinuousOn, Equicontinuous] + +lemma equicontinuous_restrict_iff (F : ι → X → α) {S : Set X} : + Equicontinuous (S.restrict ∘ F) ↔ EquicontinuousOn F S := by + simp [Equicontinuous, EquicontinuousOn, equicontinuousAt_restrict_iff] + +lemma UniformEquicontinuous.uniformEquicontinuousOn {F : ι → β → α} (H : UniformEquicontinuous F) + (S : Set β) : UniformEquicontinuousOn F S := + fun U hU ↦ (H U hU).filter_mono inf_le_left + +lemma UniformEquicontinuousOn.mono {F : ι → β → α} {S T : Set β} + (H : UniformEquicontinuousOn F T) (hST : S ⊆ T) : UniformEquicontinuousOn F S := + fun U hU ↦ (H U hU).filter_mono <| inf_le_inf_left _ <| principal_mono.mpr <| prod_mono hST hST + +lemma uniformEquicontinuousOn_univ (F : ι → β → α) : + UniformEquicontinuousOn F univ ↔ UniformEquicontinuous F := by + simp [UniformEquicontinuousOn, UniformEquicontinuous] + +lemma uniformEquicontinuous_restrict_iff (F : ι → β → α) {S : Set β} : + UniformEquicontinuous (S.restrict ∘ F) ↔ UniformEquicontinuousOn F S := by + rw [UniformEquicontinuous, UniformEquicontinuousOn] + conv in _ ⊓ _ => rw [← Subtype.range_val (s := S), ← range_prod_map, ← map_comap] + /-! ### Empty index type -/ @@ -135,16 +218,31 @@ lemma equicontinuousAt_empty [h : IsEmpty ι] (F : ι → X → α) (x₀ : X) : EquicontinuousAt F x₀ := fun _ _ ↦ eventually_of_forall (fun _ ↦ h.elim) +@[simp] +lemma equicontinuousWithinAt_empty [h : IsEmpty ι] (F : ι → X → α) (S : Set X) (x₀ : X) : + EquicontinuousWithinAt F S x₀ := + fun _ _ ↦ eventually_of_forall (fun _ ↦ h.elim) + @[simp] lemma equicontinuous_empty [IsEmpty ι] (F : ι → X → α) : Equicontinuous F := equicontinuousAt_empty F +@[simp] +lemma equicontinuousOn_empty [IsEmpty ι] (F : ι → X → α) (S : Set X) : + EquicontinuousOn F S := + fun x₀ _ ↦ equicontinuousWithinAt_empty F S x₀ + @[simp] lemma uniformEquicontinuous_empty [h : IsEmpty ι] (F : ι → β → α) : UniformEquicontinuous F := fun _ _ ↦ eventually_of_forall (fun _ ↦ h.elim) +@[simp] +lemma uniformEquicontinuousOn_empty [h : IsEmpty ι] (F : ι → β → α) (S : Set β) : + UniformEquicontinuousOn F S := + fun _ _ ↦ eventually_of_forall (fun _ ↦ h.elim) + /-! ### Finite index type -/ @@ -154,14 +252,28 @@ theorem equicontinuousAt_finite [Finite ι] {F : ι → X → α} {x₀ : X} : simp [EquicontinuousAt, ContinuousAt, (nhds_basis_uniformity' (𝓤 α).basis_sets).tendsto_right_iff, UniformSpace.ball, @forall_swap _ ι] +theorem equicontinuousWithinAt_finite [Finite ι] {F : ι → X → α} {S : Set X} {x₀ : X} : + EquicontinuousWithinAt F S x₀ ↔ ∀ i, ContinuousWithinAt (F i) S x₀ := by + simp [EquicontinuousWithinAt, ContinuousWithinAt, + (nhds_basis_uniformity' (𝓤 α).basis_sets).tendsto_right_iff, UniformSpace.ball, + @forall_swap _ ι] + theorem equicontinuous_finite [Finite ι] {F : ι → X → α} : Equicontinuous F ↔ ∀ i, Continuous (F i) := by simp only [Equicontinuous, equicontinuousAt_finite, continuous_iff_continuousAt, @forall_swap ι] +theorem equicontinuousOn_finite [Finite ι] {F : ι → X → α} {S : Set X} : + EquicontinuousOn F S ↔ ∀ i, ContinuousOn (F i) S := by + simp only [EquicontinuousOn, equicontinuousWithinAt_finite, ContinuousOn, @forall_swap ι] + theorem uniformEquicontinuous_finite [Finite ι] {F : ι → β → α} : UniformEquicontinuous F ↔ ∀ i, UniformContinuous (F i) := by simp only [UniformEquicontinuous, eventually_all, @forall_swap _ ι]; rfl +theorem uniformEquicontinuousOn_finite [Finite ι] {F : ι → β → α} {S : Set β} : + UniformEquicontinuousOn F S ↔ ∀ i, UniformContinuousOn (F i) S := by + simp only [UniformEquicontinuousOn, eventually_all, @forall_swap _ ι]; rfl + /-! ### Index type with a unique element -/ @@ -170,96 +282,180 @@ theorem equicontinuousAt_unique [Unique ι] {F : ι → X → α} {x : X} : EquicontinuousAt F x ↔ ContinuousAt (F default) x := equicontinuousAt_finite.trans Unique.forall_iff +theorem equicontinuousWithinAt_unique [Unique ι] {F : ι → X → α} {S : Set X} {x : X} : + EquicontinuousWithinAt F S x ↔ ContinuousWithinAt (F default) S x := + equicontinuousWithinAt_finite.trans Unique.forall_iff + theorem equicontinuous_unique [Unique ι] {F : ι → X → α} : Equicontinuous F ↔ Continuous (F default) := equicontinuous_finite.trans Unique.forall_iff +theorem equicontinuousOn_unique [Unique ι] {F : ι → X → α} {S : Set X} : + EquicontinuousOn F S ↔ ContinuousOn (F default) S := + equicontinuousOn_finite.trans Unique.forall_iff + theorem uniformEquicontinuous_unique [Unique ι] {F : ι → β → α} : UniformEquicontinuous F ↔ UniformContinuous (F default) := uniformEquicontinuous_finite.trans Unique.forall_iff -/-- Reformulation of equicontinuity at `x₀` comparing two variables near `x₀` instead of comparing -only one with `x₀`. -/ -theorem equicontinuousAt_iff_pair {F : ι → X → α} {x₀ : X} : - EquicontinuousAt F x₀ ↔ - ∀ U ∈ 𝓤 α, ∃ V ∈ 𝓝 x₀, ∀ x ∈ V, ∀ y ∈ V, ∀ i, (F i x, F i y) ∈ U := by +theorem uniformEquicontinuousOn_unique [Unique ι] {F : ι → β → α} {S : Set β} : + UniformEquicontinuousOn F S ↔ UniformContinuousOn (F default) S := + uniformEquicontinuousOn_finite.trans Unique.forall_iff + +/-- Reformulation of equicontinuity at `x₀` within a set `S`, comparing two variables near `x₀` +instead of comparing only one with `x₀`. -/ +theorem equicontinuousWithinAt_iff_pair {F : ι → X → α} {S : Set X} {x₀ : X} (hx₀ : x₀ ∈ S) : + EquicontinuousWithinAt F S x₀ ↔ + ∀ U ∈ 𝓤 α, ∃ V ∈ 𝓝[S] x₀, ∀ x ∈ V, ∀ y ∈ V, ∀ i, (F i x, F i y) ∈ U := by constructor <;> intro H U hU · rcases comp_symm_mem_uniformity_sets hU with ⟨V, hV, hVsymm, hVU⟩ refine' ⟨_, H V hV, fun x hx y hy i => hVU (prod_mk_mem_compRel _ (hy i))⟩ exact hVsymm.mk_mem_comm.mp (hx i) · rcases H U hU with ⟨V, hV, hVU⟩ - filter_upwards [hV] using fun x hx i => hVU x₀ (mem_of_mem_nhds hV) x hx i + filter_upwards [hV] using fun x hx i => hVU x₀ (mem_of_mem_nhdsWithin hx₀ hV) x hx i + +/-- Reformulation of equicontinuity at `x₀` comparing two variables near `x₀` instead of comparing +only one with `x₀`. -/ +theorem equicontinuousAt_iff_pair {F : ι → X → α} {x₀ : X} : + EquicontinuousAt F x₀ ↔ + ∀ U ∈ 𝓤 α, ∃ V ∈ 𝓝 x₀, ∀ x ∈ V, ∀ y ∈ V, ∀ i, (F i x, F i y) ∈ U := by + simp_rw [← equicontinuousWithinAt_univ, equicontinuousWithinAt_iff_pair (mem_univ x₀), + nhdsWithin_univ] #align equicontinuous_at_iff_pair equicontinuousAt_iff_pair /-- Uniform equicontinuity implies equicontinuity. -/ theorem UniformEquicontinuous.equicontinuous {F : ι → β → α} (h : UniformEquicontinuous F) : - Equicontinuous F := fun x₀ U hU => - mem_of_superset (ball_mem_nhds x₀ (h U hU)) fun _ hx i => hx i + Equicontinuous F := fun x₀ U hU ↦ + mem_of_superset (ball_mem_nhds x₀ (h U hU)) fun _ hx i ↦ hx i #align uniform_equicontinuous.equicontinuous UniformEquicontinuous.equicontinuous +/-- Uniform equicontinuity on a subset implies equicontinuity on that subset. -/ +theorem UniformEquicontinuousOn.equicontinuousOn {F : ι → β → α} {S : Set β} + (h : UniformEquicontinuousOn F S) : + EquicontinuousOn F S := fun _ hx₀ U hU ↦ + mem_of_superset (ball_mem_nhdsWithin hx₀ (h U hU)) fun _ hx i ↦ hx i + /-- Each function of a family equicontinuous at `x₀` is continuous at `x₀`. -/ theorem EquicontinuousAt.continuousAt {F : ι → X → α} {x₀ : X} (h : EquicontinuousAt F x₀) (i : ι) : ContinuousAt (F i) x₀ := (UniformSpace.hasBasis_nhds _).tendsto_right_iff.2 fun U ⟨hU, _⟩ ↦ (h U hU).mono fun _x hx ↦ hx i #align equicontinuous_at.continuous_at EquicontinuousAt.continuousAt +/-- Each function of a family equicontinuous at `x₀` within `S` is continuous at `x₀` within `S`. -/ +theorem EquicontinuousWithinAt.continuousWithinAt {F : ι → X → α} {S : Set X} {x₀ : X} + (h : EquicontinuousWithinAt F S x₀) (i : ι) : + ContinuousWithinAt (F i) S x₀ := + (UniformSpace.hasBasis_nhds _).tendsto_right_iff.2 fun U ⟨hU, _⟩ ↦ (h U hU).mono fun _x hx ↦ hx i + protected theorem Set.EquicontinuousAt.continuousAt_of_mem {H : Set <| X → α} {x₀ : X} (h : H.EquicontinuousAt x₀) {f : X → α} (hf : f ∈ H) : ContinuousAt f x₀ := h.continuousAt ⟨f, hf⟩ #align set.equicontinuous_at.continuous_at_of_mem Set.EquicontinuousAt.continuousAt_of_mem +protected theorem Set.EquicontinuousWithinAt.continuousWithinAt_of_mem {H : Set <| X → α} + {S : Set X} {x₀ : X} (h : H.EquicontinuousWithinAt S x₀) {f : X → α} (hf : f ∈ H) : + ContinuousWithinAt f S x₀ := + h.continuousWithinAt ⟨f, hf⟩ + /-- Each function of an equicontinuous family is continuous. -/ theorem Equicontinuous.continuous {F : ι → X → α} (h : Equicontinuous F) (i : ι) : Continuous (F i) := continuous_iff_continuousAt.mpr fun x => (h x).continuousAt i #align equicontinuous.continuous Equicontinuous.continuous +/-- Each function of a family equicontinuous on `S` is continuous on `S`. -/ +theorem EquicontinuousOn.continuousOn {F : ι → X → α} {S : Set X} (h : EquicontinuousOn F S) + (i : ι) : ContinuousOn (F i) S := + fun x hx ↦ (h x hx).continuousWithinAt i + protected theorem Set.Equicontinuous.continuous_of_mem {H : Set <| X → α} (h : H.Equicontinuous) {f : X → α} (hf : f ∈ H) : Continuous f := h.continuous ⟨f, hf⟩ #align set.equicontinuous.continuous_of_mem Set.Equicontinuous.continuous_of_mem +protected theorem Set.EquicontinuousOn.continuousOn_of_mem {H : Set <| X → α} {S : Set X} + (h : H.EquicontinuousOn S) {f : X → α} (hf : f ∈ H) : ContinuousOn f S := + h.continuousOn ⟨f, hf⟩ + /-- Each function of a uniformly equicontinuous family is uniformly continuous. -/ theorem UniformEquicontinuous.uniformContinuous {F : ι → β → α} (h : UniformEquicontinuous F) (i : ι) : UniformContinuous (F i) := fun U hU => mem_map.mpr (mem_of_superset (h U hU) fun _ hxy => hxy i) #align uniform_equicontinuous.uniform_continuous UniformEquicontinuous.uniformContinuous +/-- Each function of a family uniformly equicontinuous on `S` is uniformly continuous on `S`. -/ +theorem UniformEquicontinuousOn.uniformContinuousOn {F : ι → β → α} {S : Set β} + (h : UniformEquicontinuousOn F S) (i : ι) : + UniformContinuousOn (F i) S := fun U hU => + mem_map.mpr (mem_of_superset (h U hU) fun _ hxy => hxy i) + protected theorem Set.UniformEquicontinuous.uniformContinuous_of_mem {H : Set <| β → α} (h : H.UniformEquicontinuous) {f : β → α} (hf : f ∈ H) : UniformContinuous f := h.uniformContinuous ⟨f, hf⟩ #align set.uniform_equicontinuous.uniform_continuous_of_mem Set.UniformEquicontinuous.uniformContinuous_of_mem +protected theorem Set.UniformEquicontinuousOn.uniformContinuousOn_of_mem {H : Set <| β → α} + {S : Set β} (h : H.UniformEquicontinuousOn S) {f : β → α} (hf : f ∈ H) : + UniformContinuousOn f S := + h.uniformContinuousOn ⟨f, hf⟩ + /-- Taking sub-families preserves equicontinuity at a point. -/ theorem EquicontinuousAt.comp {F : ι → X → α} {x₀ : X} (h : EquicontinuousAt F x₀) (u : κ → ι) : EquicontinuousAt (F ∘ u) x₀ := fun U hU => (h U hU).mono fun _ H k => H (u k) #align equicontinuous_at.comp EquicontinuousAt.comp +/-- Taking sub-families preserves equicontinuity at a point within a subset. -/ +theorem EquicontinuousWithinAt.comp {F : ι → X → α} {S : Set X} {x₀ : X} + (h : EquicontinuousWithinAt F S x₀) (u : κ → ι) : + EquicontinuousWithinAt (F ∘ u) S x₀ := + fun U hU ↦ (h U hU).mono fun _ H k => H (u k) + protected theorem Set.EquicontinuousAt.mono {H H' : Set <| X → α} {x₀ : X} (h : H.EquicontinuousAt x₀) (hH : H' ⊆ H) : H'.EquicontinuousAt x₀ := h.comp (inclusion hH) #align set.equicontinuous_at.mono Set.EquicontinuousAt.mono +protected theorem Set.EquicontinuousWithinAt.mono {H H' : Set <| X → α} {S : Set X} {x₀ : X} + (h : H.EquicontinuousWithinAt S x₀) (hH : H' ⊆ H) : H'.EquicontinuousWithinAt S x₀ := + h.comp (inclusion hH) + /-- Taking sub-families preserves equicontinuity. -/ theorem Equicontinuous.comp {F : ι → X → α} (h : Equicontinuous F) (u : κ → ι) : Equicontinuous (F ∘ u) := fun x => (h x).comp u #align equicontinuous.comp Equicontinuous.comp +/-- Taking sub-families preserves equicontinuity on a subset. -/ +theorem EquicontinuousOn.comp {F : ι → X → α} {S : Set X} (h : EquicontinuousOn F S) (u : κ → ι) : + EquicontinuousOn (F ∘ u) S := fun x hx ↦ (h x hx).comp u + protected theorem Set.Equicontinuous.mono {H H' : Set <| X → α} (h : H.Equicontinuous) (hH : H' ⊆ H) : H'.Equicontinuous := h.comp (inclusion hH) #align set.equicontinuous.mono Set.Equicontinuous.mono +protected theorem Set.EquicontinuousOn.mono {H H' : Set <| X → α} {S : Set X} + (h : H.EquicontinuousOn S) (hH : H' ⊆ H) : H'.EquicontinuousOn S := + h.comp (inclusion hH) + /-- Taking sub-families preserves uniform equicontinuity. -/ theorem UniformEquicontinuous.comp {F : ι → β → α} (h : UniformEquicontinuous F) (u : κ → ι) : UniformEquicontinuous (F ∘ u) := fun U hU => (h U hU).mono fun _ H k => H (u k) #align uniform_equicontinuous.comp UniformEquicontinuous.comp +/-- Taking sub-families preserves uniform equicontinuity on a subset. -/ +theorem UniformEquicontinuousOn.comp {F : ι → β → α} {S : Set β} (h : UniformEquicontinuousOn F S) + (u : κ → ι) : UniformEquicontinuousOn (F ∘ u) S := + fun U hU ↦ (h U hU).mono fun _ H k => H (u k) + protected theorem Set.UniformEquicontinuous.mono {H H' : Set <| β → α} (h : H.UniformEquicontinuous) (hH : H' ⊆ H) : H'.UniformEquicontinuous := h.comp (inclusion hH) #align set.uniform_equicontinuous.mono Set.UniformEquicontinuous.mono +protected theorem Set.UniformEquicontinuousOn.mono {H H' : Set <| β → α} {S : Set β} + (h : H.UniformEquicontinuousOn S) (hH : H' ⊆ H) : H'.UniformEquicontinuousOn S := + h.comp (inclusion hH) + /-- A family `𝓕 : ι → X → α` is equicontinuous at `x₀` iff `range 𝓕` is equicontinuous at `x₀`, i.e the family `(↑) : range F → X → α` is equicontinuous at `x₀`. -/ theorem equicontinuousAt_iff_range {F : ι → X → α} {x₀ : X} : @@ -267,6 +463,12 @@ theorem equicontinuousAt_iff_range {F : ι → X → α} {x₀ : X} : simp only [EquicontinuousAt, forall_subtype_range_iff] #align equicontinuous_at_iff_range equicontinuousAt_iff_range +/-- A family `𝓕 : ι → X → α` is equicontinuous at `x₀` within `S` iff `range 𝓕` is equicontinuous +at `x₀` within `S`, i.e the family `(↑) : range F → X → α` is equicontinuous at `x₀` within `S`. -/ +theorem equicontinuousWithinAt_iff_range {F : ι → X → α} {S : Set X} {x₀ : X} : + EquicontinuousWithinAt F S x₀ ↔ EquicontinuousWithinAt ((↑) : range F → X → α) S x₀ := by + simp only [EquicontinuousWithinAt, forall_subtype_range_iff] + /-- A family `𝓕 : ι → X → α` is equicontinuous iff `range 𝓕` is equicontinuous, i.e the family `(↑) : range F → X → α` is equicontinuous. -/ theorem equicontinuous_iff_range {F : ι → X → α} : @@ -274,13 +476,26 @@ theorem equicontinuous_iff_range {F : ι → X → α} : forall_congr' fun _ => equicontinuousAt_iff_range #align equicontinuous_iff_range equicontinuous_iff_range +/-- A family `𝓕 : ι → X → α` is equicontinuous on `S` iff `range 𝓕` is equicontinuous on `S`, +i.e the family `(↑) : range F → X → α` is equicontinuous on `S`. -/ +theorem equicontinuousOn_iff_range {F : ι → X → α} {S : Set X} : + EquicontinuousOn F S ↔ EquicontinuousOn ((↑) : range F → X → α) S := + forall_congr' fun _ ↦ forall_congr' fun _ ↦ equicontinuousWithinAt_iff_range + /-- A family `𝓕 : ι → β → α` is uniformly equicontinuous iff `range 𝓕` is uniformly equicontinuous, i.e the family `(↑) : range F → β → α` is uniformly equicontinuous. -/ -theorem uniformEquicontinuous_at_iff_range {F : ι → β → α} : +theorem uniformEquicontinuous_iff_range {F : ι → β → α} : UniformEquicontinuous F ↔ UniformEquicontinuous ((↑) : range F → β → α) := ⟨fun h => by rw [← comp_rangeSplitting F]; exact h.comp _, fun h => h.comp (rangeFactorization F)⟩ -#align uniform_equicontinuous_at_iff_range uniformEquicontinuous_at_iff_range +#align uniform_equicontinuous_at_iff_range uniformEquicontinuous_iff_range + +/-- A family `𝓕 : ι → β → α` is uniformly equicontinuous on `S` iff `range 𝓕` is uniformly +equicontinuous on `S`, i.e the family `(↑) : range F → β → α` is uniformly equicontinuous on `S`. -/ +theorem uniformEquicontinuousOn_iff_range {F : ι → β → α} {S : Set β} : + UniformEquicontinuousOn F S ↔ UniformEquicontinuousOn ((↑) : range F → β → α) S := + ⟨fun h => by rw [← comp_rangeSplitting F]; exact h.comp _, fun h => + h.comp (rangeFactorization F)⟩ section @@ -296,6 +511,16 @@ theorem equicontinuousAt_iff_continuousAt {F : ι → X → α} {x₀ : X} : rfl #align equicontinuous_at_iff_continuous_at equicontinuousAt_iff_continuousAt +/-- A family `𝓕 : ι → X → α` is equicontinuous at `x₀` within `S` iff the function +`swap 𝓕 : X → ι → α` is continuous at `x₀` within `S` +*when `ι → α` is equipped with the topology of uniform convergence*. This is very useful for +developping the equicontinuity API, but it should not be used directly for other purposes. -/ +theorem equicontinuousWithinAt_iff_continuousWithinAt {F : ι → X → α} {S : Set X} {x₀ : X} : + EquicontinuousWithinAt F S x₀ ↔ + ContinuousWithinAt (ofFun ∘ Function.swap F : X → ι →ᵤ α) S x₀ := by + rw [ContinuousWithinAt, (UniformFun.hasBasis_nhds ι α _).tendsto_right_iff] + rfl + /-- A family `𝓕 : ι → X → α` is equicontinuous iff the function `swap 𝓕 : X → ι → α` is continuous *when `ι → α` is equipped with the topology of uniform convergence*. This is very useful for developping the equicontinuity API, but it should not be used directly for other @@ -305,6 +530,14 @@ theorem equicontinuous_iff_continuous {F : ι → X → α} : simp_rw [Equicontinuous, continuous_iff_continuousAt, equicontinuousAt_iff_continuousAt] #align equicontinuous_iff_continuous equicontinuous_iff_continuous +/-- A family `𝓕 : ι → X → α` is equicontinuous on `S` iff the function `swap 𝓕 : X → ι → α` is +continuous on `S` *when `ι → α` is equipped with the topology of uniform convergence*. This is +very useful for developping the equicontinuity API, but it should not be used directly for other +purposes. -/ +theorem equicontinuousOn_iff_continuousOn {F : ι → X → α} {S : Set X} : + EquicontinuousOn F S ↔ ContinuousOn (ofFun ∘ Function.swap F : X → ι →ᵤ α) S := by + simp_rw [EquicontinuousOn, ContinuousOn, equicontinuousWithinAt_iff_continuousWithinAt] + /-- A family `𝓕 : ι → β → α` is uniformly equicontinuous iff the function `swap 𝓕 : β → ι → α` is uniformly continuous *when `ι → α` is equipped with the uniform structure of uniform convergence*. This is very useful for developping the equicontinuity API, but it should not be used directly @@ -315,54 +548,103 @@ theorem uniformEquicontinuous_iff_uniformContinuous {F : ι → β → α} : rfl #align uniform_equicontinuous_iff_uniform_continuous uniformEquicontinuous_iff_uniformContinuous -theorem equicontinuousAt_iInf_rng {α' : Type*} {u : κ → UniformSpace α'} {F : ι → X → α'} - {x₀ : X} : - @EquicontinuousAt _ _ _ _ (⨅ k, u k) F x₀ ↔ ∀ k, @EquicontinuousAt _ _ _ _ (u k) F x₀ := by - simp only [@equicontinuousAt_iff_continuousAt _ _ _ _ _, topologicalSpace] - unfold ContinuousAt +/-- A family `𝓕 : ι → β → α` is uniformly equicontinuous on `S` iff the function +`swap 𝓕 : β → ι → α` is uniformly continuous on `S` +*when `ι → α` is equipped with the uniform structure of uniform convergence*. This is very useful +for developping the equicontinuity API, but it should not be used directly for other purposes. -/ +theorem uniformEquicontinuousOn_iff_uniformContinuousOn {F : ι → β → α} {S : Set β} : + UniformEquicontinuousOn F S ↔ UniformContinuousOn (ofFun ∘ Function.swap F : β → ι →ᵤ α) S := by + rw [UniformContinuousOn, (UniformFun.hasBasis_uniformity ι α).tendsto_right_iff] + rfl + +theorem equicontinuousWithinAt_iInf_rng {u : κ → UniformSpace α'} {F : ι → X → α'} + {S : Set X} {x₀ : X} : EquicontinuousWithinAt (uα := ⨅ k, u k) F S x₀ ↔ + ∀ k, EquicontinuousWithinAt (uα := u k) F S x₀ := by + simp only [equicontinuousWithinAt_iff_continuousWithinAt (uα := _), topologicalSpace] + unfold ContinuousWithinAt rw [UniformFun.iInf_eq, toTopologicalSpace_iInf, nhds_iInf, tendsto_iInf] -theorem equicontinuous_iInf_rng {α' : Type*} {u : κ → UniformSpace α'} {F : ι → X → α'} : - @Equicontinuous _ _ _ _ (⨅ k, u k) F ↔ ∀ k, @Equicontinuous _ _ _ _ (u k) F := by - simp_rw [@equicontinuous_iff_continuous _ _ _ _ _, UniformFun.topologicalSpace] +theorem equicontinuousAt_iInf_rng {u : κ → UniformSpace α'} {F : ι → X → α'} + {x₀ : X} : + EquicontinuousAt (uα := ⨅ k, u k) F x₀ ↔ ∀ k, EquicontinuousAt (uα := u k) F x₀ := by + simp only [← equicontinuousWithinAt_univ (uα := _), equicontinuousWithinAt_iInf_rng] + +theorem equicontinuous_iInf_rng {u : κ → UniformSpace α'} {F : ι → X → α'} : + Equicontinuous (uα := ⨅ k, u k) F ↔ ∀ k, Equicontinuous (uα := u k) F := by + simp_rw [equicontinuous_iff_continuous (uα := _), UniformFun.topologicalSpace] rw [UniformFun.iInf_eq, toTopologicalSpace_iInf, continuous_iInf_rng] -theorem uniformEquicontinuous_iInf_rng {α' : Type*} {u : κ → UniformSpace α'} {F : ι → β → α'} : - @UniformEquicontinuous _ _ _ (⨅ k, u k) _ F ↔ ∀ k, @UniformEquicontinuous _ _ _ (u k) _ F := by - simp_rw [@uniformEquicontinuous_iff_uniformContinuous _ _ _ _] +theorem equicontinuousOn_iInf_rng {u : κ → UniformSpace α'} {F : ι → X → α'} + {S : Set X} : + EquicontinuousOn (uα := ⨅ k, u k) F S ↔ ∀ k, EquicontinuousOn (uα := u k) F S := by + simp_rw [EquicontinuousOn, equicontinuousWithinAt_iInf_rng, @forall_swap _ κ] + +theorem uniformEquicontinuous_iInf_rng {u : κ → UniformSpace α'} {F : ι → β → α'} : + UniformEquicontinuous (uα := ⨅ k, u k) F ↔ ∀ k, UniformEquicontinuous (uα := u k) F := by + simp_rw [uniformEquicontinuous_iff_uniformContinuous (uα := _)] rw [UniformFun.iInf_eq, uniformContinuous_iInf_rng] -theorem equicontinuousAt_iInf_dom {X' : Type*} {t : κ → TopologicalSpace X'} {F : ι → X' → α} - {x₀ : X'} {k : κ} (hk : @EquicontinuousAt _ _ _ (t k) _ F x₀) : - @EquicontinuousAt _ _ _ (⨅ k, t k) _ F x₀ := by - simp? [@equicontinuousAt_iff_continuousAt _ _ _ _] at hk ⊢ says - simp only [@equicontinuousAt_iff_continuousAt _ _ _ _] at hk ⊢ - unfold ContinuousAt at hk ⊢ +theorem uniformEquicontinuousOn_iInf_rng {u : κ → UniformSpace α'} {F : ι → β → α'} + {S : Set β} : UniformEquicontinuousOn (uα := ⨅ k, u k) F S ↔ + ∀ k, UniformEquicontinuousOn (uα := u k) F S := by + simp_rw [uniformEquicontinuousOn_iff_uniformContinuousOn (uα := _)] + unfold UniformContinuousOn + rw [UniformFun.iInf_eq, iInf_uniformity, tendsto_iInf] + +theorem equicontinuousWithinAt_iInf_dom {t : κ → TopologicalSpace X'} {F : ι → X' → α} + {S : Set X'} {x₀ : X'} {k : κ} (hk : EquicontinuousWithinAt (tX := t k) F S x₀) : + EquicontinuousWithinAt (tX := ⨅ k, t k) F S x₀ := by + simp [equicontinuousWithinAt_iff_continuousWithinAt (tX := _)] at hk ⊢ + unfold ContinuousWithinAt nhdsWithin at hk ⊢ rw [nhds_iInf] - exact tendsto_iInf' k hk - -theorem equicontinuous_iInf_dom {X' : Type*} {t : κ → TopologicalSpace X'} {F : ι → X' → α} - {k : κ} (hk : @Equicontinuous _ _ _ (t k) _ F) : - @Equicontinuous _ _ _ (⨅ k, t k) _ F := by - simp_rw [@equicontinuous_iff_continuous _ _ _ _] at hk ⊢ - exact continuous_iInf_dom hk - -theorem uniform_equicontinuous_infi_dom {β' : Type*} {u : κ → UniformSpace β'} {F : ι → β' → α} - {k : κ} (hk : @UniformEquicontinuous _ _ _ _ (u k) F) : - @UniformEquicontinuous _ _ _ _ (⨅ k, u k) F := by - simp_rw [@uniformEquicontinuous_iff_uniformContinuous _ _ _ _ _] at hk ⊢ + exact hk.mono_left <| inf_le_inf_right _ <| iInf_le _ k + +theorem equicontinuousAt_iInf_dom {t : κ → TopologicalSpace X'} {F : ι → X' → α} + {x₀ : X'} {k : κ} (hk : EquicontinuousAt (tX := t k) F x₀) : + EquicontinuousAt (tX := ⨅ k, t k) F x₀ := by + rw [← equicontinuousWithinAt_univ (tX := _)] at hk ⊢ + exact equicontinuousWithinAt_iInf_dom hk + +theorem equicontinuous_iInf_dom {t : κ → TopologicalSpace X'} {F : ι → X' → α} + {k : κ} (hk : Equicontinuous (tX := t k) F) : + Equicontinuous (tX := ⨅ k, t k) F := + fun x ↦ equicontinuousAt_iInf_dom (hk x) + +theorem equicontinuousOn_iInf_dom {t : κ → TopologicalSpace X'} {F : ι → X' → α} + {S : Set X'} {k : κ} (hk : EquicontinuousOn (tX := t k) F S) : + EquicontinuousOn (tX := ⨅ k, t k) F S := + fun x hx ↦ equicontinuousWithinAt_iInf_dom (hk x hx) + +theorem uniformEquicontinuous_iInf_dom {u : κ → UniformSpace β'} {F : ι → β' → α} + {k : κ} (hk : UniformEquicontinuous (uβ := u k) F) : + UniformEquicontinuous (uβ := ⨅ k, u k) F := by + simp_rw [uniformEquicontinuous_iff_uniformContinuous (uβ := _)] at hk ⊢ exact uniformContinuous_iInf_dom hk -theorem Filter.HasBasis.equicontinuousAt_iff_left {κ : Type*} {p : κ → Prop} {s : κ → Set X} +theorem uniformEquicontinuousOn_iInf_dom {u : κ → UniformSpace β'} {F : ι → β' → α} + {S : Set β'} {k : κ} (hk : UniformEquicontinuousOn (uβ := u k) F S) : + UniformEquicontinuousOn (uβ := ⨅ k, u k) F S := by + simp_rw [uniformEquicontinuousOn_iff_uniformContinuousOn (uβ := _)] at hk ⊢ + unfold UniformContinuousOn + rw [iInf_uniformity] + exact hk.mono_left <| inf_le_inf_right _ <| iInf_le _ k + +theorem Filter.HasBasis.equicontinuousAt_iff_left {p : κ → Prop} {s : κ → Set X} {F : ι → X → α} {x₀ : X} (hX : (𝓝 x₀).HasBasis p s) : EquicontinuousAt F x₀ ↔ ∀ U ∈ 𝓤 α, ∃ k, p k ∧ ∀ x ∈ s k, ∀ i, (F i x₀, F i x) ∈ U := by rw [equicontinuousAt_iff_continuousAt, ContinuousAt, hX.tendsto_iff (UniformFun.hasBasis_nhds ι α _)] - simp only [Function.comp_apply, mem_setOf_eq, exists_prop] rfl #align filter.has_basis.equicontinuous_at_iff_left Filter.HasBasis.equicontinuousAt_iff_left -theorem Filter.HasBasis.equicontinuousAt_iff_right {κ : Type*} {p : κ → Prop} {s : κ → Set (α × α)} +theorem Filter.HasBasis.equicontinuousWithinAt_iff_left {p : κ → Prop} {s : κ → Set X} + {F : ι → X → α} {S : Set X} {x₀ : X} (hX : (𝓝[S] x₀).HasBasis p s) : + EquicontinuousWithinAt F S x₀ ↔ ∀ U ∈ 𝓤 α, ∃ k, p k ∧ ∀ x ∈ s k, ∀ i, (F i x₀, F i x) ∈ U := by + rw [equicontinuousWithinAt_iff_continuousWithinAt, ContinuousWithinAt, + hX.tendsto_iff (UniformFun.hasBasis_nhds ι α _)] + rfl + +theorem Filter.HasBasis.equicontinuousAt_iff_right {p : κ → Prop} {s : κ → Set (α × α)} {F : ι → X → α} {x₀ : X} (hα : (𝓤 α).HasBasis p s) : EquicontinuousAt F x₀ ↔ ∀ k, p k → ∀ᶠ x in 𝓝 x₀, ∀ i, (F i x₀, F i x) ∈ s k := by rw [equicontinuousAt_iff_continuousAt, ContinuousAt, @@ -370,6 +652,13 @@ theorem Filter.HasBasis.equicontinuousAt_iff_right {κ : Type*} {p : κ → Prop rfl #align filter.has_basis.equicontinuous_at_iff_right Filter.HasBasis.equicontinuousAt_iff_right +theorem Filter.HasBasis.equicontinuousWithinAt_iff_right {p : κ → Prop} + {s : κ → Set (α × α)} {F : ι → X → α} {S : Set X} {x₀ : X} (hα : (𝓤 α).HasBasis p s) : + EquicontinuousWithinAt F S x₀ ↔ ∀ k, p k → ∀ᶠ x in 𝓝[S] x₀, ∀ i, (F i x₀, F i x) ∈ s k := by + rw [equicontinuousWithinAt_iff_continuousWithinAt, ContinuousWithinAt, + (UniformFun.hasBasis_nhds_of_basis ι α _ hα).tendsto_right_iff] + rfl + theorem Filter.HasBasis.equicontinuousAt_iff {κ₁ κ₂ : Type*} {p₁ : κ₁ → Prop} {s₁ : κ₁ → Set X} {p₂ : κ₂ → Prop} {s₂ : κ₂ → Set (α × α)} {F : ι → X → α} {x₀ : X} (hX : (𝓝 x₀).HasBasis p₁ s₁) (hα : (𝓤 α).HasBasis p₂ s₂) : @@ -377,21 +666,38 @@ theorem Filter.HasBasis.equicontinuousAt_iff {κ₁ κ₂ : Type*} {p₁ : κ₁ ∀ k₂, p₂ k₂ → ∃ k₁, p₁ k₁ ∧ ∀ x ∈ s₁ k₁, ∀ i, (F i x₀, F i x) ∈ s₂ k₂ := by rw [equicontinuousAt_iff_continuousAt, ContinuousAt, hX.tendsto_iff (UniformFun.hasBasis_nhds_of_basis ι α _ hα)] - simp only [Function.comp_apply, mem_setOf_eq, exists_prop] rfl #align filter.has_basis.equicontinuous_at_iff Filter.HasBasis.equicontinuousAt_iff -theorem Filter.HasBasis.uniformEquicontinuous_iff_left {κ : Type*} {p : κ → Prop} +theorem Filter.HasBasis.equicontinuousWithinAt_iff {κ₁ κ₂ : Type*} {p₁ : κ₁ → Prop} + {s₁ : κ₁ → Set X} {p₂ : κ₂ → Prop} {s₂ : κ₂ → Set (α × α)} {F : ι → X → α} {S : Set X} {x₀ : X} + (hX : (𝓝[S] x₀).HasBasis p₁ s₁) (hα : (𝓤 α).HasBasis p₂ s₂) : + EquicontinuousWithinAt F S x₀ ↔ + ∀ k₂, p₂ k₂ → ∃ k₁, p₁ k₁ ∧ ∀ x ∈ s₁ k₁, ∀ i, (F i x₀, F i x) ∈ s₂ k₂ := by + rw [equicontinuousWithinAt_iff_continuousWithinAt, ContinuousWithinAt, + hX.tendsto_iff (UniformFun.hasBasis_nhds_of_basis ι α _ hα)] + rfl + +theorem Filter.HasBasis.uniformEquicontinuous_iff_left {p : κ → Prop} {s : κ → Set (β × β)} {F : ι → β → α} (hβ : (𝓤 β).HasBasis p s) : UniformEquicontinuous F ↔ ∀ U ∈ 𝓤 α, ∃ k, p k ∧ ∀ x y, (x, y) ∈ s k → ∀ i, (F i x, F i y) ∈ U := by rw [uniformEquicontinuous_iff_uniformContinuous, UniformContinuous, hβ.tendsto_iff (UniformFun.hasBasis_uniformity ι α)] - simp only [Prod.forall, Function.comp_apply, mem_setOf_eq, exists_prop] + simp only [Prod.forall] rfl #align filter.has_basis.uniform_equicontinuous_iff_left Filter.HasBasis.uniformEquicontinuous_iff_left -theorem Filter.HasBasis.uniformEquicontinuous_iff_right {κ : Type*} {p : κ → Prop} +theorem Filter.HasBasis.uniformEquicontinuousOn_iff_left {p : κ → Prop} + {s : κ → Set (β × β)} {F : ι → β → α} {S : Set β} (hβ : (𝓤 β ⊓ 𝓟 (S ×ˢ S)).HasBasis p s) : + UniformEquicontinuousOn F S ↔ + ∀ U ∈ 𝓤 α, ∃ k, p k ∧ ∀ x y, (x, y) ∈ s k → ∀ i, (F i x, F i y) ∈ U := by + rw [uniformEquicontinuousOn_iff_uniformContinuousOn, UniformContinuousOn, + hβ.tendsto_iff (UniformFun.hasBasis_uniformity ι α)] + simp only [Prod.forall] + rfl + +theorem Filter.HasBasis.uniformEquicontinuous_iff_right {p : κ → Prop} {s : κ → Set (α × α)} {F : ι → β → α} (hα : (𝓤 α).HasBasis p s) : UniformEquicontinuous F ↔ ∀ k, p k → ∀ᶠ xy : β × β in 𝓤 β, ∀ i, (F i xy.1, F i xy.2) ∈ s k := by rw [uniformEquicontinuous_iff_uniformContinuous, UniformContinuous, @@ -399,6 +705,14 @@ theorem Filter.HasBasis.uniformEquicontinuous_iff_right {κ : Type*} {p : κ → rfl #align filter.has_basis.uniform_equicontinuous_iff_right Filter.HasBasis.uniformEquicontinuous_iff_right +theorem Filter.HasBasis.uniformEquicontinuousOn_iff_right {p : κ → Prop} + {s : κ → Set (α × α)} {F : ι → β → α} {S : Set β} (hα : (𝓤 α).HasBasis p s) : + UniformEquicontinuousOn F S ↔ + ∀ k, p k → ∀ᶠ xy : β × β in 𝓤 β ⊓ 𝓟 (S ×ˢ S), ∀ i, (F i xy.1, F i xy.2) ∈ s k := by + rw [uniformEquicontinuousOn_iff_uniformContinuousOn, UniformContinuousOn, + (UniformFun.hasBasis_uniformity_of_basis ι α hα).tendsto_right_iff] + rfl + theorem Filter.HasBasis.uniformEquicontinuous_iff {κ₁ κ₂ : Type*} {p₁ : κ₁ → Prop} {s₁ : κ₁ → Set (β × β)} {p₂ : κ₂ → Prop} {s₂ : κ₂ → Set (α × α)} {F : ι → β → α} (hβ : (𝓤 β).HasBasis p₁ s₁) (hα : (𝓤 α).HasBasis p₂ s₂) : @@ -406,12 +720,22 @@ theorem Filter.HasBasis.uniformEquicontinuous_iff {κ₁ κ₂ : Type*} {p₁ : ∀ k₂, p₂ k₂ → ∃ k₁, p₁ k₁ ∧ ∀ x y, (x, y) ∈ s₁ k₁ → ∀ i, (F i x, F i y) ∈ s₂ k₂ := by rw [uniformEquicontinuous_iff_uniformContinuous, UniformContinuous, hβ.tendsto_iff (UniformFun.hasBasis_uniformity_of_basis ι α hα)] - simp only [Prod.forall, Function.comp_apply, mem_setOf_eq, exists_prop] + simp only [Prod.forall] rfl #align filter.has_basis.uniform_equicontinuous_iff Filter.HasBasis.uniformEquicontinuous_iff +theorem Filter.HasBasis.uniformEquicontinuousOn_iff {κ₁ κ₂ : Type*} {p₁ : κ₁ → Prop} + {s₁ : κ₁ → Set (β × β)} {p₂ : κ₂ → Prop} {s₂ : κ₂ → Set (α × α)} {F : ι → β → α} + {S : Set β} (hβ : (𝓤 β ⊓ 𝓟 (S ×ˢ S)).HasBasis p₁ s₁) (hα : (𝓤 α).HasBasis p₂ s₂) : + UniformEquicontinuousOn F S ↔ + ∀ k₂, p₂ k₂ → ∃ k₁, p₁ k₁ ∧ ∀ x y, (x, y) ∈ s₁ k₁ → ∀ i, (F i x, F i y) ∈ s₂ k₂ := by + rw [uniformEquicontinuousOn_iff_uniformContinuousOn, UniformContinuousOn, + hβ.tendsto_iff (UniformFun.hasBasis_uniformity_of_basis ι α hα)] + simp only [Prod.forall] + rfl + /-- Given `u : α → β` a uniform inducing map, a family `𝓕 : ι → X → α` is equicontinuous at a point -`x₀ : X` iff the family `𝓕'`, obtained by precomposing each function of `𝓕` by `u`, is +`x₀ : X` iff the family `𝓕'`, obtained by composing each function of `𝓕` by `u`, is equicontinuous at `x₀`. -/ theorem UniformInducing.equicontinuousAt_iff {F : ι → X → α} {x₀ : X} {u : α → β} (hu : UniformInducing u) : EquicontinuousAt F x₀ ↔ EquicontinuousAt ((u ∘ ·) ∘ F) x₀ := by @@ -420,110 +744,255 @@ theorem UniformInducing.equicontinuousAt_iff {F : ι → X → α} {x₀ : X} {u rfl #align uniform_inducing.equicontinuous_at_iff UniformInducing.equicontinuousAt_iff +/-- Given `u : α → β` a uniform inducing map, a family `𝓕 : ι → X → α` is equicontinuous at a point +`x₀ : X` within a subset `S : Set X` iff the family `𝓕'`, obtained by composing each function +of `𝓕` by `u`, is equicontinuous at `x₀` within `S`. -/ +theorem UniformInducing.equicontinuousWithinAt_iff {F : ι → X → α} {S : Set X} {x₀ : X} {u : α → β} + (hu : UniformInducing u) : EquicontinuousWithinAt F S x₀ ↔ + EquicontinuousWithinAt ((u ∘ ·) ∘ F) S x₀ := by + have := (UniformFun.postcomp_uniformInducing (α := ι) hu).inducing + simp only [equicontinuousWithinAt_iff_continuousWithinAt, this.continuousWithinAt_iff] + rfl + /-- Given `u : α → β` a uniform inducing map, a family `𝓕 : ι → X → α` is equicontinuous iff the -family `𝓕'`, obtained by precomposing each function of `𝓕` by `u`, is equicontinuous. -/ +family `𝓕'`, obtained by composing each function of `𝓕` by `u`, is equicontinuous. -/ theorem UniformInducing.equicontinuous_iff {F : ι → X → α} {u : α → β} (hu : UniformInducing u) : Equicontinuous F ↔ Equicontinuous ((u ∘ ·) ∘ F) := by congrm ∀ x, ?_ rw [hu.equicontinuousAt_iff] #align uniform_inducing.equicontinuous_iff UniformInducing.equicontinuous_iff +/-- Given `u : α → β` a uniform inducing map, a family `𝓕 : ι → X → α` is equicontinuous on a +subset `S : Set X` iff the family `𝓕'`, obtained by composing each function of `𝓕` by `u`, is +equicontinuous on `S`. -/ +theorem UniformInducing.equicontinuousOn_iff {F : ι → X → α} {S : Set X} {u : α → β} + (hu : UniformInducing u) : EquicontinuousOn F S ↔ EquicontinuousOn ((u ∘ ·) ∘ F) S := by + congrm ∀ x ∈ S, ?_ + rw [hu.equicontinuousWithinAt_iff] + /-- Given `u : α → γ` a uniform inducing map, a family `𝓕 : ι → β → α` is uniformly equicontinuous -iff the family `𝓕'`, obtained by precomposing each function of `𝓕` by `u`, is uniformly +iff the family `𝓕'`, obtained by composing each function of `𝓕` by `u`, is uniformly equicontinuous. -/ theorem UniformInducing.uniformEquicontinuous_iff {F : ι → β → α} {u : α → γ} (hu : UniformInducing u) : UniformEquicontinuous F ↔ UniformEquicontinuous ((u ∘ ·) ∘ F) := by have := UniformFun.postcomp_uniformInducing (α := ι) hu - rw [uniformEquicontinuous_iff_uniformContinuous, uniformEquicontinuous_iff_uniformContinuous, - this.uniformContinuous_iff] + simp only [uniformEquicontinuous_iff_uniformContinuous, this.uniformContinuous_iff] rfl #align uniform_inducing.uniform_equicontinuous_iff UniformInducing.uniformEquicontinuous_iff -/-- A version of `EquicontinuousAt.closure` applicable to subsets of types which embed continuously -into `X → α` with the product topology. It turns out we don't need any other condition on the -embedding than continuity, but in practice this will mostly be applied to `DFunLike` types where -the coercion is injective. -/ -theorem EquicontinuousAt.closure' {A : Set Y} {u : Y → X → α} {x₀ : X} - (hA : EquicontinuousAt (u ∘ (↑) : A → X → α) x₀) (hu : Continuous u) : - EquicontinuousAt (u ∘ (↑) : closure A → X → α) x₀ := by +/-- Given `u : α → γ` a uniform inducing map, a family `𝓕 : ι → β → α` is uniformly equicontinuous +on a subset `S : Set β` iff the family `𝓕'`, obtained by composing each function of `𝓕` by `u`, +is uniformly equicontinuous on `S`. -/ +theorem UniformInducing.uniformEquicontinuousOn_iff {F : ι → β → α} {S : Set β} {u : α → γ} + (hu : UniformInducing u) : + UniformEquicontinuousOn F S ↔ UniformEquicontinuousOn ((u ∘ ·) ∘ F) S := by + have := UniformFun.postcomp_uniformInducing (α := ι) hu + simp only [uniformEquicontinuousOn_iff_uniformContinuousOn, this.uniformContinuousOn_iff] + rfl + +/-- If a set of functions is equicontinuous at some `x₀` within a set `S`, the same is true for its +closure in *any* topology for which evaluation at any `x ∈ S ∪ {x₀}` is continuous. Since +this will be applied to `DFunLike` types, we state it for any topological space whith a map +to `X → α` satisfying the right continuity conditions. See also `Set.EquicontinuousWithinAt.closure` +for a more familiar (but weaker) statement. + +Note: This could *technically* be called `EquicontinuousWithinAt.closure` without name clashes +with `Set.EquicontinuousWithinAt.closure`, but we don't do it because, even with a `protected` +marker, it would introduce ambiguities while working in namespace `Set` (e.g, in the proof of +any theorem called `Set.something`). -/ +theorem EquicontinuousWithinAt.closure' {A : Set Y} {u : Y → X → α} {S : Set X} {x₀ : X} + (hA : EquicontinuousWithinAt (u ∘ (↑) : A → X → α) S x₀) (hu₁ : Continuous (S.restrict ∘ u)) + (hu₂ : Continuous (eval x₀ ∘ u)) : + EquicontinuousWithinAt (u ∘ (↑) : closure A → X → α) S x₀ := by intro U hU rcases mem_uniformity_isClosed hU with ⟨V, hV, hVclosed, hVU⟩ - filter_upwards [hA V hV] with x hx + filter_upwards [hA V hV, eventually_mem_nhdsWithin] with x hx hxS rw [SetCoe.forall] at * change A ⊆ (fun f => (u f x₀, u f x)) ⁻¹' V at hx - refine' (closure_minimal hx <| hVclosed.preimage <| _).trans (preimage_mono hVU) - exact Continuous.prod_mk ((continuous_apply x₀).comp hu) ((continuous_apply x).comp hu) + refine (closure_minimal hx <| hVclosed.preimage <| hu₂.prod_mk ?_).trans (preimage_mono hVU) + exact (continuous_apply ⟨x, hxS⟩).comp hu₁ + +/-- If a set of functions is equicontinuous at some `x₀`, the same is true for its closure in *any* +topology for which evaluation at any point is continuous. Since this will be applied to +`DFunLike` types, we state it for any topological space whith a map to `X → α` satisfying the right +continuity conditions. See also `Set.EquicontinuousAt.closure` for a more familiar statement. -/ +theorem EquicontinuousAt.closure' {A : Set Y} {u : Y → X → α} {x₀ : X} + (hA : EquicontinuousAt (u ∘ (↑) : A → X → α) x₀) (hu : Continuous u) : + EquicontinuousAt (u ∘ (↑) : closure A → X → α) x₀ := by + rw [← equicontinuousWithinAt_univ] at hA ⊢ + exact hA.closure' (Pi.continuous_restrict _ |>.comp hu) (continuous_apply x₀ |>.comp hu) #align equicontinuous_at.closure' EquicontinuousAt.closure' /-- If a set of functions is equicontinuous at some `x₀`, its closure for the product topology is also equicontinuous at `x₀`. -/ -protected theorem EquicontinuousAt.closure {A : Set (X → α)} {x₀ : X} (hA : A.EquicontinuousAt x₀) : - (closure A).EquicontinuousAt x₀ := - EquicontinuousAt.closure' (u := id) hA continuous_id -#align equicontinuous_at.closure EquicontinuousAt.closure - -/-- If `𝓕 : ι → X → α` tends to `f : X → α` *pointwise* along some nontrivial filter, and if the -family `𝓕` is equicontinuous at some `x₀ : X`, then the limit is continuous at `x₀`. -/ -theorem Filter.Tendsto.continuousAt_of_equicontinuousAt {l : Filter ι} [l.NeBot] {F : ι → X → α} - {f : X → α} {x₀ : X} (h₁ : Tendsto F l (𝓝 f)) (h₂ : EquicontinuousAt F x₀) : - ContinuousAt f x₀ := - (equicontinuousAt_iff_range.mp h₂).closure.continuousAt - ⟨f, mem_closure_of_tendsto h₁ <| eventually_of_forall mem_range_self⟩ -#align filter.tendsto.continuous_at_of_equicontinuous_at Filter.Tendsto.continuousAt_of_equicontinuousAt - -/-- A version of `Equicontinuous.closure` applicable to subsets of types which embed continuously -into `X → α` with the product topology. It turns out we don't need any other condition on the -embedding than continuity, but in practice this will mostly be applied to `DFunLike` types where -the coercion is injective. -/ +protected theorem Set.EquicontinuousAt.closure {A : Set (X → α)} {x₀ : X} + (hA : A.EquicontinuousAt x₀) : (closure A).EquicontinuousAt x₀ := + hA.closure' (u := id) continuous_id +#align equicontinuous_at.closure Set.EquicontinuousAt.closure + +/-- If a set of functions is equicontinuous at some `x₀` within a set `S`, its closure for the +product topology is also equicontinuous at `x₀` within `S`. This would also be true for the coarser +topology of pointwise convergence on `S ∪ {x₀}`, see `Set.EquicontinuousWithinAt.closure'`. -/ +protected theorem Set.EquicontinuousWithinAt.closure {A : Set (X → α)} {S : Set X} {x₀ : X} + (hA : A.EquicontinuousWithinAt S x₀) : + (closure A).EquicontinuousWithinAt S x₀ := + hA.closure' (u := id) (Pi.continuous_restrict _) (continuous_apply _) + +/-- If a set of functions is equicontinuous, the same is true for its closure in *any* +topology for which evaluation at any point is continuous. Since this will be applied to +`DFunLike` types, we state it for any topological space whith a map to `X → α` satisfying the right +continuity conditions. See also `Set.Equicontinuous.closure` for a more familiar statement. -/ theorem Equicontinuous.closure' {A : Set Y} {u : Y → X → α} (hA : Equicontinuous (u ∘ (↑) : A → X → α)) (hu : Continuous u) : - Equicontinuous (u ∘ (↑) : closure A → X → α) := fun x => (hA x).closure' hu + Equicontinuous (u ∘ (↑) : closure A → X → α) := fun x ↦ (hA x).closure' hu #align equicontinuous.closure' Equicontinuous.closure' +/-- If a set of functions is equicontinuous on a set `S`, the same is true for its closure in *any* +topology for which evaluation at any `x ∈ S` is continuous. Since this will be applied to +`DFunLike` types, we state it for any topological space whith a map to `X → α` satisfying the right +continuity conditions. See also `Set.EquicontinuousOn.closure` for a more familiar +(but weaker) statement. -/ +theorem EquicontinuousOn.closure' {A : Set Y} {u : Y → X → α} {S : Set X} + (hA : EquicontinuousOn (u ∘ (↑) : A → X → α) S) (hu : Continuous (S.restrict ∘ u)) : + EquicontinuousOn (u ∘ (↑) : closure A → X → α) S := + fun x hx ↦ (hA x hx).closure' hu <| by exact continuous_apply ⟨x, hx⟩ |>.comp hu + /-- If a set of functions is equicontinuous, its closure for the product topology is also equicontinuous. -/ -theorem Equicontinuous.closure {A : Set <| X → α} (hA : A.Equicontinuous) : - (closure A).Equicontinuous := fun x => (hA x).closure -#align equicontinuous.closure Equicontinuous.closure +protected theorem Set.Equicontinuous.closure {A : Set <| X → α} (hA : A.Equicontinuous) : + (closure A).Equicontinuous := fun x ↦ Set.EquicontinuousAt.closure (hA x) +#align equicontinuous.closure Set.Equicontinuous.closure -/-- If `𝓕 : ι → X → α` tends to `f : X → α` *pointwise* along some nontrivial filter, and if the -family `𝓕` is equicontinuous, then the limit is continuous. -/ -theorem Filter.Tendsto.continuous_of_equicontinuousAt {l : Filter ι} [l.NeBot] {F : ι → X → α} - {f : X → α} (h₁ : Tendsto F l (𝓝 f)) (h₂ : Equicontinuous F) : Continuous f := - continuous_iff_continuousAt.mpr fun x => h₁.continuousAt_of_equicontinuousAt (h₂ x) -#align filter.tendsto.continuous_of_equicontinuous_at Filter.Tendsto.continuous_of_equicontinuousAt - -/-- A version of `UniformEquicontinuous.closure` applicable to subsets of types which embed -continuously into `β → α` with the product topology. It turns out we don't need any other condition -on the embedding than continuity, but in practice this will mostly be applied to `DFunLike` types -where the coercion is injective. -/ -theorem UniformEquicontinuous.closure' {A : Set Y} {u : Y → β → α} - (hA : UniformEquicontinuous (u ∘ (↑) : A → β → α)) (hu : Continuous u) : - UniformEquicontinuous (u ∘ (↑) : closure A → β → α) := by +/-- If a set of functions is equicontinuous, its closure for the product topology is also +equicontinuous. This would also be true for the coarser topology of pointwise convergence on `S`, +see `EquicontinuousOn.closure'`. -/ +protected theorem Set.EquicontinuousOn.closure {A : Set <| X → α} {S : Set X} + (hA : A.EquicontinuousOn S) : (closure A).EquicontinuousOn S := + fun x hx ↦ Set.EquicontinuousWithinAt.closure (hA x hx) + +/-- If a set of functions is uniformly equicontinuous on a set `S`, the same is true for its +closure in *any* topology for which evaluation at any `x ∈ S` i continuous. Since this will be +applied to `DFunLike` types, we state it for any topological space whith a map to `β → α` satisfying +the right continuity conditions. See also `Set.UniformEquicontinuousOn.closure` for a more familiar +(but weaker) statement. -/ +theorem UniformEquicontinuousOn.closure' {A : Set Y} {u : Y → β → α} {S : Set β} + (hA : UniformEquicontinuousOn (u ∘ (↑) : A → β → α) S) (hu : Continuous (S.restrict ∘ u)) : + UniformEquicontinuousOn (u ∘ (↑) : closure A → β → α) S := by intro U hU rcases mem_uniformity_isClosed hU with ⟨V, hV, hVclosed, hVU⟩ - filter_upwards [hA V hV] - rintro ⟨x, y⟩ hxy + filter_upwards [hA V hV, mem_inf_of_right (mem_principal_self _)] + rintro ⟨x, y⟩ hxy ⟨hxS, hyS⟩ rw [SetCoe.forall] at * change A ⊆ (fun f => (u f x, u f y)) ⁻¹' V at hxy - refine' (closure_minimal hxy <| hVclosed.preimage <| _).trans (preimage_mono hVU) - exact Continuous.prod_mk ((continuous_apply x).comp hu) ((continuous_apply y).comp hu) + refine (closure_minimal hxy <| hVclosed.preimage <| .prod_mk ?_ ?_).trans (preimage_mono hVU) + · exact (continuous_apply ⟨x, hxS⟩).comp hu + · exact (continuous_apply ⟨y, hyS⟩).comp hu + +/-- If a set of functions is uniformly equicontinuous, the same is true for its closure in *any* +topology for which evaluation at any point is continuous. Since this will be applied to +`DFunLike` types, we state it for any topological space whith a map to `β → α` satisfying the right +continuity conditions. See also `Set.UniformEquicontinuous.closure` for a more familiar statement. +-/ +theorem UniformEquicontinuous.closure' {A : Set Y} {u : Y → β → α} + (hA : UniformEquicontinuous (u ∘ (↑) : A → β → α)) (hu : Continuous u) : + UniformEquicontinuous (u ∘ (↑) : closure A → β → α) := by + rw [← uniformEquicontinuousOn_univ] at hA ⊢ + exact hA.closure' (Pi.continuous_restrict _ |>.comp hu) #align uniform_equicontinuous.closure' UniformEquicontinuous.closure' /-- If a set of functions is uniformly equicontinuous, its closure for the product topology is also uniformly equicontinuous. -/ -theorem UniformEquicontinuous.closure {A : Set <| β → α} (hA : A.UniformEquicontinuous) : - (closure A).UniformEquicontinuous := +protected theorem Set.UniformEquicontinuous.closure {A : Set <| β → α} + (hA : A.UniformEquicontinuous) : (closure A).UniformEquicontinuous := UniformEquicontinuous.closure' (u := id) hA continuous_id -#align uniform_equicontinuous.closure UniformEquicontinuous.closure +#align uniform_equicontinuous.closure Set.UniformEquicontinuous.closure + +/-- If a set of functions is uniformly equicontinuous on a set `S`, its closure for the product +topology is also uniformly equicontinuous. This would also be true for the coarser topology of +pointwise convergence on `S`, see `UniformEquicontinuousOn.closure'`.-/ +protected theorem Set.UniformEquicontinuousOn.closure {A : Set <| β → α} {S : Set β} + (hA : A.UniformEquicontinuousOn S) : (closure A).UniformEquicontinuousOn S := + UniformEquicontinuousOn.closure' (u := id) hA (Pi.continuous_restrict _) + +/- +Implementation note: The following lemma (as well as all the following variations) could +theoretically be deduced from the "closure" statements above. For example, we could do: +```lean +theorem Filter.Tendsto.continuousAt_of_equicontinuousAt {l : Filter ι} [l.NeBot] {F : ι → X → α} + {f : X → α} {x₀ : X} (h₁ : Tendsto F l (𝓝 f)) (h₂ : EquicontinuousAt F x₀) : + ContinuousAt f x₀ := + (equicontinuousAt_iff_range.mp h₂).closure.continuousAt + ⟨f, mem_closure_of_tendsto h₁ <| eventually_of_forall mem_range_self⟩ -/-- If `𝓕 : ι → β → α` tends to `f : β → α` *pointwise* along some nontrivial filter, and if the -family `𝓕` is uniformly equicontinuous, then the limit is uniformly continuous. -/ theorem Filter.Tendsto.uniformContinuous_of_uniformEquicontinuous {l : Filter ι} [l.NeBot] {F : ι → β → α} {f : β → α} (h₁ : Tendsto F l (𝓝 f)) (h₂ : UniformEquicontinuous F) : UniformContinuous f := - (uniformEquicontinuous_at_iff_range.mp h₂).closure.uniformContinuous + (uniformEquicontinuous_iff_range.mp h₂).closure.uniformContinuous ⟨f, mem_closure_of_tendsto h₁ <| eventually_of_forall mem_range_self⟩ +``` + +Unfortunately, the proofs get painful when dealing with the relative case as one needs to change +the ambient topology. So it turns out to be easier to re-do the proof by hand. +-/ + +/-- If `𝓕 : ι → X → α` tends to `f : X → α` *pointwise on `S ∪ {x₀} : Set X`* along some nontrivial +filter, and if the family `𝓕` is equicontinuous at `x₀ : X` within `S`, then the limit is +continuous at `x₀` within `S`. -/ +theorem Filter.Tendsto.continuousWithinAt_of_equicontinuousWithinAt {l : Filter ι} [l.NeBot] + {F : ι → X → α} {f : X → α} {S : Set X} {x₀ : X} (h₁ : ∀ x ∈ S, Tendsto (F · x) l (𝓝 (f x))) + (h₂ : Tendsto (F · x₀) l (𝓝 (f x₀))) (h₃ : EquicontinuousWithinAt F S x₀) : + ContinuousWithinAt f S x₀ := by + intro U hU; rw [mem_map] + rcases UniformSpace.mem_nhds_iff.mp hU with ⟨V, hV, hVU⟩ + rcases mem_uniformity_isClosed hV with ⟨W, hW, hWclosed, hWV⟩ + filter_upwards [h₃ W hW, eventually_mem_nhdsWithin] with x hx hxS using + hVU <| ball_mono hWV (f x₀) <| hWclosed.mem_of_tendsto (h₂.prod_mk_nhds (h₁ x hxS)) <| + eventually_of_forall hx + +/-- If `𝓕 : ι → X → α` tends to `f : X → α` *pointwise* along some nontrivial filter, and if the +family `𝓕` is equicontinuous at some `x₀ : X`, then the limit is continuous at `x₀`. -/ +theorem Filter.Tendsto.continuousAt_of_equicontinuousAt {l : Filter ι} [l.NeBot] {F : ι → X → α} + {f : X → α} {x₀ : X} (h₁ : Tendsto F l (𝓝 f)) (h₂ : EquicontinuousAt F x₀) : + ContinuousAt f x₀ := by + rw [← continuousWithinAt_univ, ← equicontinuousWithinAt_univ, tendsto_pi_nhds] at * + exact continuousWithinAt_of_equicontinuousWithinAt (fun x _ ↦ h₁ x) (h₁ x₀) h₂ +#align filter.tendsto.continuous_at_of_equicontinuous_at Filter.Tendsto.continuousAt_of_equicontinuousAt + +/-- If `𝓕 : ι → X → α` tends to `f : X → α` *pointwise* along some nontrivial filter, and if the +family `𝓕` is equicontinuous, then the limit is continuous. -/ +theorem Filter.Tendsto.continuous_of_equicontinuous {l : Filter ι} [l.NeBot] {F : ι → X → α} + {f : X → α} (h₁ : Tendsto F l (𝓝 f)) (h₂ : Equicontinuous F) : Continuous f := + continuous_iff_continuousAt.mpr fun x => h₁.continuousAt_of_equicontinuousAt (h₂ x) +#align filter.tendsto.continuous_of_equicontinuous_at Filter.Tendsto.continuous_of_equicontinuous + +/-- If `𝓕 : ι → X → α` tends to `f : X → α` *pointwise on `S : Set X`* along some nontrivial +filter, and if the family `𝓕` is equicontinuous, then the limit is continuous on `S`. -/ +theorem Filter.Tendsto.continuousOn_of_equicontinuousOn {l : Filter ι} [l.NeBot] {F : ι → X → α} + {f : X → α} {S : Set X} (h₁ : ∀ x ∈ S, Tendsto (F · x) l (𝓝 (f x))) + (h₂ : EquicontinuousOn F S) : ContinuousOn f S := + fun x hx ↦ Filter.Tendsto.continuousWithinAt_of_equicontinuousWithinAt h₁ (h₁ x hx) (h₂ x hx) + +/-- If `𝓕 : ι → β → α` tends to `f : β → α` *pointwise on `S : Set β`* along some nontrivial +filter, and if the family `𝓕` is uniformly equicontinuous on `S`, then the limit is uniformly +continuous on `S`. -/ +theorem Filter.Tendsto.uniformContinuousOn_of_uniformEquicontinuousOn {l : Filter ι} [l.NeBot] + {F : ι → β → α} {f : β → α} {S : Set β} (h₁ : ∀ x ∈ S, Tendsto (F · x) l (𝓝 (f x))) + (h₂ : UniformEquicontinuousOn F S) : + UniformContinuousOn f S := by + intro U hU; rw [mem_map] + rcases mem_uniformity_isClosed hU with ⟨V, hV, hVclosed, hVU⟩ + filter_upwards [h₂ V hV, mem_inf_of_right (mem_principal_self _)] + rintro ⟨x, y⟩ hxy ⟨hxS, hyS⟩ + exact hVU <| hVclosed.mem_of_tendsto ((h₁ x hxS).prod_mk_nhds (h₁ y hyS)) <| + eventually_of_forall hxy + +/-- If `𝓕 : ι → β → α` tends to `f : β → α` *pointwise* along some nontrivial filter, and if the +family `𝓕` is uniformly equicontinuous, then the limit is uniformly continuous. -/ +theorem Filter.Tendsto.uniformContinuous_of_uniformEquicontinuous {l : Filter ι} [l.NeBot] + {F : ι → β → α} {f : β → α} (h₁ : Tendsto F l (𝓝 f)) (h₂ : UniformEquicontinuous F) : + UniformContinuous f := by + rw [← uniformContinuousOn_univ, ← uniformEquicontinuousOn_univ, tendsto_pi_nhds] at * + exact uniformContinuousOn_of_uniformEquicontinuousOn (fun x _ ↦ h₁ x) h₂ #align filter.tendsto.uniform_continuous_of_uniform_equicontinuous Filter.Tendsto.uniformContinuous_of_uniformEquicontinuous /-- If `F : ι → X → α` is a family of functions equicontinuous at `x`,