TendstoLocallyUniformly — Mathlib

English

Locally uniform convergence on the whole space is equivalent to local uniform convergence on every subset when the set is univ.

Русский

Локальная равномерная сходимость на всём пространстве эквивалентна локальной равномерной сходимости на любом подмножестве в случае унив.

LaTeX

$$TendstoLocallyUniformlyOn F f p univ ↔ TendstoLocallyUniformly F f p$$

Lean4

/-- A sequence of functions `Fₙ` converges locally uniformly to a limiting function `f` with respect
to a filter `p` if, for any entourage of the diagonal `u`, for any `x`, one has `p`-eventually
`(f y, Fₙ y) ∈ u` for all `y` in a neighborhood of `x`. -/
def TendstoLocallyUniformly (F : ι → α → β) (f : α → β) (p : Filter ι) :=
  ∀ u ∈ 𝓤 β, ∀ x : α, ∃ t ∈ 𝓝 x, ∀ᶠ n in p, ∀ y ∈ t, (f y, F n y) ∈ u

Похожие утверждения