prod_union_eq_left — Mathlib

English

For finite s1, s2 and a predicate that makes certain elements vanish, the product over s1 ∪ s2 equals the product over s1 when the extra elements contribute 1.

Русский

При конечных s1, s2 и условии, делающее некоторые элементы нулевыми, произведение по s1 ∪ s2 равно произведению по s1, если добавленные элементы дают 1.

LaTeX

$$$\prod a\in s1 \cup s2, f a = \prod a\in s1, f a$$$

Lean4

@[to_additive]
theorem prod_union_eq_left [DecidableEq ι] (hs : ∀ a ∈ s₂, a ∉ s₁ → f a = 1) : ∏ a ∈ s₁ ∪ s₂, f a = ∏ a ∈ s₁, f a :=
  Eq.symm <| prod_subset subset_union_left fun _a ha ha' ↦ hs _ ((mem_union.1 ha).resolve_left ha') ha'

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