hasProd_prod_of_ne_finset_one — Mathlib

English

If f is 1 outside finite set s, then HasProd f (s.prod f) L.

Русский

Если f вне конечного множества s равна 1, тогда HasProd f (произведение по s) L.

LaTeX

$$$ \forall b ∉ s, f(b)=1 \rightarrow HasProd f (s.prod (\lambda b, f b)) L $$$

Lean4

/-- If a function `f` is `1` outside of a finite set `s`, then it `HasProd` `∏ b ∈ s, f b`. -/
@[to_additive /-- If a function `f` vanishes outside of a finite set `s`, then it `HasSum`
    `∑ b ∈ s, f b`. -/
    ]
theorem hasProd_prod_of_ne_finset_one (hf : ∀ b ∉ s, f b = 1) [L.LeAtTop] : HasProd f (∏ b ∈ s, f b) L :=
  ((hasProd_subtype_iff_of_mulSupport_subset <| mulSupport_subset_iff'.2 hf).1 <| s.hasProd f) |>.mono_left L.le_atTop

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