congr_right — Mathlib

English

If F_n converges locally uniformly to f on s along p, and f equals g on s, then F_n converges locally uniformly to g on s along p.

Русский

Если F_n сходится локально равномерно к f на s по p, и f= g на s, тогда F_n сходится к g локально равномерно на s по p.

LaTeX

$$$\ TendstoLocallyUniformlyOn F f p s \land s.EqOn f g \Rightarrow \ TendstoLocallyUniformlyOn F g p s$$$

Lean4

theorem congr_right {g : α → β} (hf : TendstoLocallyUniformlyOn F f p s) (hg : s.EqOn f g) :
    TendstoLocallyUniformlyOn F g 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 hy.1 ▸ hi y hy.2

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