Uniform convergence to a constant

Stream: Is there code for X?

[Vincent Beffara]

Are these in Mathlib already?

import Mathlib

open Topology Filter Uniformity Uniform MeasureTheory Set

variable {α β ι : Type*} [MeasurableSpace α] [TopologicalSpace α] [UniformSpace β]

lemma tendstoUniformly_iff_nhds (p : Filter ι) (F : ι → α → β) (b : β) :
    TendstoUniformly F (fun _ => b) p ↔ ∀ s ∈ 𝓝 b, ∀ᶠ i in p, ∀ a, F i a ∈ s := by
  refine ⟨fun h s hs => ?_, fun h u hu => h _ (UniformSpace.ball_mem_nhds _ hu)⟩
  obtain ⟨v, h1, h2⟩ := UniformSpace.mem_nhds_iff.mp hs
  filter_upwards [h v h1] with i h x using h2 (h x)

lemma tendstoUniformlyOnFilter_iff_nhds (p : Filter ι) (q : Filter α) (b : β) :
    TendstoUniformlyOnFilter F (fun _ => b) p q ↔ ∀ s ∈ 𝓝 b, ∀ᶠ n in p ×ˢ q, F n.1 n.2 ∈ s := by
  refine ⟨fun h s hs => ?_, fun h u hu => h _ (UniformSpace.ball_mem_nhds b hu)⟩
  obtain ⟨v, hv, h2⟩ := UniformSpace.mem_nhds_iff.mp hs
  filter_upwards [h v hv] with n hn using h2 hn

Sometimes it can be useful to speak about uniform convergence to a value rather than a function, and this makes sense without a uniform space structure.