prod_eq_single_of_mem — Mathlib

English

If only one element of s remains after filtering to a, the product reduces to f(a).

Русский

Если после фильтрации остаётся единственный элемент a, произведение упрощается до f(a).

LaTeX

$$$\prod x\in s, f x = f a$$$

Lean4

@[to_additive]
theorem prod_eq_single_of_mem {s : Finset ι} {f : ι → M} (a : ι) (h : a ∈ s) (h₀ : ∀ b ∈ s, b ≠ a → f b = 1) :
    ∏ x ∈ s, f x = f a := by
  calc
    ∏ x ∈ s, f x = ∏ x ∈ { a }, f x := by {
      refine (prod_subset ?_ ?_).symm
      · intro _ H
        rwa [mem_singleton.1 H]
      · simpa only [mem_singleton]
    }
    _ = f a := prod_singleton _ _

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