prod_dite_of_true — Mathlib

English

If p is true for all i ∈ s, then the product of dite equals the product of the f-part, mirroring the previous form.

Русский

Если p истинно по всем i∈s, произведение dite равно произведению f-части.

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_true {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, f i.1 (h _ i.2) := by
  refine prod_bij' (fun x hx => ⟨x, hx⟩) (fun x _ ↦ x) ?_ ?_ ?_ ?_ ?_ <;> aesop

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