tprod_eq_tprod_diff_singleton — Mathlib

English

If f(b) = 1, then the tprod over s equals the tprod over s minus {b}: ∏' a : s, f a = ∏' a : (s \\ {b}), f a.

Русский

Если f(b) = 1, то т-произведение по s равно т-произведению по s без {b}.

LaTeX

$$$\\\\prod' a : s, f a = \\\\prod' a : (s \\ { b } : Set β), f a$$$

Lean4

/-- If `f b = 1`, then the product of `f a` with `a ∈ s` is the same as the product of `f a` for
`a ∈ s ∖ {b}`. -/
@[to_additive /-- If `f b = 0`, then the sum of `f a` with `a ∈ s` is the same as the sum of `f a`
    for `a ∈ s ∖ {b}`. -/
    ]
theorem tprod_eq_tprod_diff_singleton {f : β → α} (s : Set β) {b : β} (hf₀ : f b = 1) :
    ∏' a : s, f a = ∏' a : (s \ { b } : Set β), f a :=
  tprod_setElem_eq_tprod_setElem_diff s { b } fun _ ha ↦ ha ▸ hf₀

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