prod_union_eq_right — Mathlib

English

Symmetric statement to the left union rule; swapping s1 and s2 yields the same equality under corresponding hypotheses.

Русский

Симметричное утверждение к правилу левого объединения; при аналогичных условиях справедливо и для правого объединения.

LaTeX

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

Lean4

@[to_additive]
theorem prod_union_eq_right [DecidableEq ι] (hs : ∀ a ∈ s₁, a ∉ s₂ → f a = 1) : ∏ a ∈ s₁ ∪ s₂, f a = ∏ a ∈ s₂, f a := by
  rw [union_comm, prod_union_eq_left hs]

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