finprod_mem_inter_mul_diff — Mathlib

English

If s ⊆ t and t is finite, then (∏ᶠ i ∈ s, f i) · (∏ᶠ i ∈ t \\ s, f i) = ∏ᶠ i ∈ t, f i.

Русский

Если s ⊆ t и t конечно, то произведение по s и произведение по t\\s перемножаются в произведение по t.

LaTeX

$$$\\Big(\\prod^\\!i \\in s, f(i)\\Big) \\cdot \\Big(\\prod^\\!i \\in t \\setminus s, f(i)\\Big) = \\prod^\\!i \\in t, f(i)$$$

Lean4

@[to_additive]
theorem finprod_mem_inter_mul_diff (t : Set α) (h : s.Finite) :
    ((∏ᶠ i ∈ s ∩ t, f i) * ∏ᶠ i ∈ s \ t, f i) = ∏ᶠ i ∈ s, f i :=
  finprod_mem_inter_mul_diff' _ <| h.inter_of_left _

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