finprod_mem_eq_prod_of_subset — Mathlib

English

For f : α → M, if h1 : s ∩ mulSupport f ⊆ t and h2 : t ⊆ s, then ∏ᶠ i ∈ s, f i = ∏ i ∈ t, f i.

Русский

Пусть для f: α → M выполнено s ∩ mulSupport f ⊆ t и t ⊆ s; тогда ∏ᶠ i ∈ s, f i = ∏ i ∈ t, f i.

LaTeX

$$$$ \prod^{\mathrm{fin}}_{i \in s} f(i) = \prod_{i \\in t} f(i). $$$$

Lean4

@[to_additive]
theorem finprod_mem_eq_prod_of_subset (f : α → M) {s : Set α} {t : Finset α} (h₁ : s ∩ mulSupport f ⊆ t) (h₂ : ↑t ⊆ s) :
    ∏ᶠ i ∈ s, f i = ∏ i ∈ t, f i :=
  finprod_cond_eq_prod_of_cond_iff _ fun hx => ⟨fun h => h₁ ⟨h, hx⟩, fun h => h₂ h⟩

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