prod_apply_ite_of_true — Mathlib

English

If s contains a, then the product of a single index equals the corresponding value; otherwise it is the identity element.

Русский

Если s содержит a, то произведение по x∈s ite (a=x) (b x) 1 равно b a; иначе 1.

LaTeX

$$$(\\prod x \\in s, \\text{ite} (a = x) (b x) 1) = b a$ при $a ∈ s$.$$

Lean4

@[to_additive]
theorem prod_apply_ite_of_true {p : ι → Prop} [DecidablePred p] (f g : ι → γ) (k : γ → M) (h : ∀ x ∈ s, p x) :
    (∏ x ∈ s, k (if p x then f x else g x)) = ∏ x ∈ s, k (f x) :=
  by
  simp_rw [apply_ite k]
  exact prod_ite_of_true h _ _

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