hasProd — Mathlib

English

If HasProdUniformlyOn f g 𝔖 holds, hs ∈ 𝔖 and hx ∈ s, then the localized product HasProd (f · x) (g x) holds.

Русский

Если HasProdUniformlyOn f g 𝔖, hs ∈ 𝔖 и hx ∈ s, тогда имеет место HasProd (f · x) (g x).

LaTeX

$$$ HasProdUniformlyOn\ f\ g\ 𝔖 \land hs\in 𝔖 \land hx\in s \Rightarrow HasProd (f\cdot x) (g x) $$$

Lean4

@[to_additive]
theorem hasProd (h : HasProdUniformlyOn f g 𝔖) (hs : s ∈ 𝔖) (hx : x ∈ s) : HasProd (f · x) (g x) :=
  (hasProdUniformlyOn_iff_tendstoUniformlyOn.mp h s hs).tendsto_at hx

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