congr — Mathlib

English

If TendstoUniformlyOn F f p s holds and F and F' coincide on s eventually (on p), then TendstoUniformlyOn F' f p s also holds.

Русский

Если F сходится равномерно на s и F нy F' совпадают на s почти наверняка, то F' также сходится равномерно на s.

LaTeX

$$$\\ TendstoUniformlyOn F f p s \\land (\\forall^\\! n \\in p, \\text{EqOn}(F n, F' n) s) \Rightarrow TendstoUniformlyOn F' f p s$$$

Lean4

theorem congr {F' : ι → α → β} (hf : TendstoUniformlyOnFilter F f p p')
    (hff' : ∀ᶠ n : ι × α in p ×ˢ p', F n.fst n.snd = F' n.fst n.snd) : TendstoUniformlyOnFilter F' f p p' :=
  by
  refine fun u hu => ((hf u hu).and hff').mono fun n h => ?_
  rw [← h.right]
  exact h.left

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