tendstoLocallyUniformlyOn_iff_filter

English

Equivalence between TendstoLocallyUniformlyOn and TendstoUniformlyOnFilter with nhdsWithin.

Русский

Эквивалентность между TendstoLocallyUniformlyOn и TendstoUniformlyOnFilter через nhdsWithin.

LaTeX

$$$$\operatorname{tendstoLocallyUniformlyOn\_iff\_filter}:\ TendstoLocallyUniformlyOn F f p s \iff \forall x\in s,\ TendstoUniformlyOnFilter F f p (\mathcal{N}_{s} x).$$$$

Lean4

theorem tendstoLocallyUniformlyOn_iff_filter :
    TendstoLocallyUniformlyOn F f p s ↔ ∀ x ∈ s, TendstoUniformlyOnFilter F f p (𝓝[s] x) :=
  by
  simp only [TendstoUniformlyOnFilter, eventually_prod_iff]
  constructor
  · rintro h x hx u hu
    obtain ⟨s, hs1, hs2⟩ := h u hu x hx
    exact ⟨_, hs2, _, eventually_of_mem hs1 fun x => id, fun hi y hy => hi y hy⟩
  · rintro h u hu x hx
    obtain ⟨pa, hpa, pb, hpb, h⟩ := h x hx u hu
    exact ⟨pb, hpb, eventually_of_mem hpa fun i hi y hy => h hi hy⟩

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