prod_ite_eq_ite_exists — Mathlib

English

For a finite type with Fintype, ∏ i, ite(p i) a 1 = ite(∃ i, p i) a 1.

Русский

Для конечного типа верно: ∏_{i} ite(p_i) a 1 = ite(∃ i, p_i) a 1.

LaTeX

$$$\\displaystyle \\prod_{i} \\operatorname{ite}(p(i))\,a\,1 = \\operatorname{ite}\\left(\\exists i, p(i)\\right) a\,1$$$

Lean4

@[to_additive]
theorem prod_ite_eq_ite_exists (p : ι → Prop) [DecidablePred p] (h : ∀ i j, p i → p j → i = j) (a : M) :
    ∏ i, ite (p i) a 1 = ite (∃ i, p i) a 1 := by simp [prod_ite_one univ p (by simpa using h)]

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