English
A TendstoUniformlyOnFilter property is preserved under restricting the domain to a subset via a restriction map.
Русский
Свойство TendstoUniformlyOnFilter сохраняется при ограничении области определения через отображение ограничения.
LaTeX
$$$$\\text{TendstoUniformlyOnFilter}(F,f,p,s)\\Rightarrow\\text{TendstoUniformlyOnFilter}(\\lambda i x. F i x, \\lambda x. f x, p, s).$$$$
Lean4
/-- A sequence of functions `Fₙ` converges uniformly on a set `s` to a limiting function `f` with
respect to the filter `p` if, for any entourage of the diagonal `u`, one has `p`-eventually
`(f x, Fₙ x) ∈ u` for all `x ∈ s`. -/
def TendstoUniformlyOn (F : ι → α → β) (f : α → β) (p : Filter ι) (s : Set α) :=
∀ u ∈ 𝓤 β, ∀ᶠ n in p, ∀ x : α, x ∈ s → (f x, F n x) ∈ u
