congr_right — Mathlib

English

If HasProdUniformlyOn f g 𝔖 and g is uniformly equal to g' on each s∈𝔖, then HasProdUniformlyOn f g' 𝔖.

Русский

Если HasProdUniformlyOn f g 𝔖 и g равномерно эквивалентно g' на каждом s∈𝔖, то HasProdUniformlyOn f g' 𝔖.

LaTeX

$$$ HasProdUniformlyOn\ f\ g\ 𝔖 \to (\forall s\in 𝔖, EqOn\ g\ g'\ s) \Rightarrow HasProdUniformlyOn\ f\ g'\ 𝔖 $$$

Lean4

@[to_additive]
theorem congr_right {g' : β → α} (h : HasProdUniformlyOn f g 𝔖) (hgg' : ∀ s ∈ 𝔖, Set.EqOn g g' s) :
    HasProdUniformlyOn f g' 𝔖 := by
  rw [hasProdUniformlyOn_iff_tendstoUniformlyOn] at *
  exact fun s hs ↦ TendstoUniformlyOn.congr_right (h s hs) (hgg' s hs)

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