prod_apply_ite_of_false — Mathlib

English

A variant of the dite equality with explicit equality in the second argument, yielding a product equal to the filtered one.

Русский

Вариант равенства dite с явным равенством во втором аргументе, приводящий произведение к отфильтрованному произведению.

LaTeX

$$$\\prod_{i \\in s} (\\text{if } h : i = a \\text{ then } b(i,h) \\text{ else } 1) = \\text{ite}(a \\in s)(b(a)\\,\\dots) 1.$$$

Lean4

@[to_additive]
theorem prod_apply_ite_of_false {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 (g x) :=
  by
  simp_rw [apply_ite k]
  exact prod_ite_of_false h _ _

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