prod_ite_index — Mathlib

English

Specialization of prod_nbij' with explicit i and j maps providing a rearrangement between s and t.

Русский

Специализация prod_nbij' с явными отображениями i и j, обеспечивающими переупорядочивание между s и t.

LaTeX

$$$\\forall i j\\; (hi):\\; \\;\\Rightarrow \\; \\prod_{x∈s} f x = \\prod_{x∈t} g x$$$

Lean4

@[to_additive]
theorem prod_ite_index (p : Prop) [Decidable p] (s t : Finset ι) (f : ι → M) :
    ∏ x ∈ if p then s else t, f x = if p then ∏ x ∈ s, f x else ∏ x ∈ t, f x :=
  apply_ite (fun s => ∏ x ∈ s, f x) _ _ _

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