congr — Mathlib

English

If F tends to f locally uniformly on p over s, and if G is pointwise equal to F on s (i.e., F n and G n coincide on s for all n), then G also tends locally uniformly to f on s.

Русский

Если F стремится локально равномерно к f по p на s, и G совпадает с F на s по каждому индексу, тогда G тоже стремится локально равномерно к f на s.

LaTeX

$$TendstoLocallyUniformlyOn F f p s → (∀ n, s.EqOn (F n) (G n)) → TendstoLocallyUniformlyOn G f p s$$

Lean4

theorem congr {G : ι → α → β} (hf : TendstoLocallyUniformlyOn F f p s) (hg : ∀ n, s.EqOn (F n) (G n)) :
    TendstoLocallyUniformlyOn G f p s := by
  rintro u hu x hx
  obtain ⟨t, ht, h⟩ := hf u hu x hx
  refine ⟨s ∩ t, inter_mem self_mem_nhdsWithin ht, ?_⟩
  filter_upwards [h] with i hi y hy using hg i hy.1 ▸ hi y hy.2

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