prod_eq_ite — Mathlib

English

Let a be any element; if a ∈ s then ∏ x∈s f x = f a else equals 1, given that all other elements are 1.

Русский

Пусть a произвольный; если a ∈ s, тогда ∏ x∈s f x = f a, иначе = 1 при условии, что для остальных элементов f равны 1.

LaTeX

$$$\prod x\in s, f x = \text{if } a\in s\text{ then } f a\text{ else } 1$$$

Lean4

@[to_additive]
theorem prod_eq_ite [DecidableEq ι] {s : Finset ι} {f : ι → M} (a : ι) (h₀ : ∀ b ∈ s, b ≠ a → f b = 1) :
    ∏ x ∈ s, f x = if a ∈ s then f a else 1 := by
  by_cases h : a ∈ s
  · simp [Finset.prod_eq_single_of_mem a h h₀, h]
  · replace h₀ : ∀ b ∈ s, f b = 1 := by aesop
    simp +contextual [h₀]

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