congr_right — Mathlib

English

If TendstoUniformlyOn F f p s holds and f and g agree on s, then TendstoUniformlyOn F g p s holds.

Русский

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

LaTeX

$$TendstoUniformlyOn F f p s ∧ EqOn f g s ⇒ TendstoUniformlyOn F g p s$$

Lean4

theorem congr_right {g : α → β} (hf : TendstoUniformlyOn F f p s) (hfg : EqOn f g s) : TendstoUniformlyOn F g p s :=
  fun u hu => by filter_upwards [hf u hu] with i hi a ha using hfg ha ▸ hi a ha

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