prod_dite_of_false — Mathlib

English

If for every i ∈ s, p(i) is true, then the product of the dite expression equals the product of the f-part over s.

Русский

Если для всех i∈s выполняется p(i) = истина, то произведение dite равно произведению f(i) по i∈s.

LaTeX

$$$\\prod_{i \\in s} (\\text{if } p(i) \\text{ then } f(i) \\text{ else } g(i)) = \\prod_{i \\in s} f(i).$$$

Lean4

@[to_additive]
theorem prod_dite_of_false {p : ι → Prop} [DecidablePred p] (h : ∀ i ∈ s, ¬p i) (f : ∀ i, p i → M) (g : ∀ i, ¬p i → M) :
    ∏ i ∈ s, (if hi : p i then f i hi else g i hi) = ∏ i : s, g i.1 (h _ i.2) := by
  refine prod_bij' (fun x hx => ⟨x, hx⟩) (fun x _ ↦ x) ?_ ?_ ?_ ?_ ?_ <;> aesop

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