MultipliableLocallyUniformlyOn_congr

English

If for every i, f i ≡ f' i on s, and h is MultipliableLocallyUniformlyOn f s, then MultipliableLocallyUniformlyOn f' s.

Русский

Если для каждого i f i совпадает с f' i на s, и h = MultipliableLocallyUniformlyOn f s, тогда MultipliableLocallyUniformlyOn f' s.

LaTeX

$$$ [T2Space α] (h : MultipliableLocallyUniformlyOn f s) (\forall i, s.EqOn (f i) (f' i)) : MultipliableLocallyUniformlyOn f' s $$$

Lean4

@[to_additive]
theorem MultipliableLocallyUniformlyOn_congr [T2Space α] {f f' : ι → β → α} (h : ∀ i, s.EqOn (f i) (f' i))
    (h2 : MultipliableLocallyUniformlyOn f s) : MultipliableLocallyUniformlyOn f' s :=
  by
  apply HasProdLocallyUniformlyOn.multipliableLocallyUniformlyOn
  exact (h2.hasProdLocallyUniformlyOn).congr fun v ↦ eqOn_fun_finsetProd h v

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