hasProd_subtype_mulSupport — Mathlib

English

For a function f, HasProd on the subtype mulSupport f is equivalent to HasProd on f itself; restricting to the mulSupport set does not lose convergence of the product.

Русский

Для функции f HasProd на подтипе mulSupport f эквивалентен HasProd на f; ограничение к mulSupport не теряет сведение произведения к пределу.

LaTeX

$$$\text{HasProd } (f\circ (↑) : mulSupport f \to α) \;\iff\; \text{HasProd } f \ a$$$

Lean4

@[to_additive (attr := simp)]
theorem hasProd_subtype_mulSupport : HasProd (f ∘ (↑) : mulSupport f → α) a ↔ HasProd f a :=
  hasProd_subtype_iff_of_mulSupport_subset <| Set.Subset.refl _

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