finprod_mem_inter_mul_diff' — Mathlib

English

For any s, t, the product over s ∩ t times the product over s \\ t equals the product over s.

Русский

Для любых s, t верно: произведение по s ∩ t умноженное на произведение по s \\ t дает произведение по s.

LaTeX

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

Lean4

@[to_additive]
theorem finprod_mem_inter_mul_diff' (t : Set α) (h : (s ∩ mulSupport f).Finite) :
    ((∏ᶠ i ∈ s ∩ t, f i) * ∏ᶠ i ∈ s \ t, f i) = ∏ᶠ i ∈ s, f i :=
  by
  rw [← finprod_mem_union', inter_union_diff]
  · rw [disjoint_iff_inf_le]
    exact fun x hx => hx.2.2 hx.1.2
  exacts [h.subset fun x hx => ⟨hx.1.1, hx.2⟩, h.subset fun x hx => ⟨hx.1.1, hx.2⟩]

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