multipliable — Mathlib

English

If h is MultipliableUniformlyOn f 𝔖, then HasProdUniformlyOn f (∏' i, f i ·) 𝔖 holds.

Русский

Если h = MultipliableUniformlyOn f 𝔖, тогда HasProdUniformlyOn f (∏' i, f i ·) 𝔖 выполняется.

LaTeX

$$$ [T2Space α] (h : MultipliableUniformlyOn f 𝔖) : HasProdUniformlyOn f (\prod' i, f i ·) 𝔖 $$$

Lean4

@[to_additive]
theorem multipliable (h : MultipliableUniformlyOn f 𝔖) (hs : s ∈ 𝔖) (hx : x ∈ s) : Multipliable (f · x) :=
  match h.exists with
  | ⟨_, hg⟩ => (hg.hasProd hs hx).multipliable

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