hasProd — Mathlib

English

For a family f: ι → ∀x, Xx and target g: ∀x, Xx, HasProd f g L is equivalent to HasProd (fun i => f i x) (g x) L for every x.

Русский

Для семейства f и g: HasProd f g L эквивалентно HasProd (f i x) (g x) для каждого x.

LaTeX

$$$\\operatorname{HasProd} f g L \\iff \\forall x, \\operatorname{HasProd}(\\lambda i, f i x) (g x) L$$$

Lean4

@[to_additive]
theorem hasProd {f : ι → ∀ x, X x} {g : ∀ x, X x} : HasProd f g L ↔ ∀ x, HasProd (fun i ↦ f i x) (g x) L := by
  simp only [HasProd, tendsto_pi_nhds, prod_apply]

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