prod_ite_irrel — Mathlib

English

Specialization of prod_bij with an index bijection e : ι → κ.

Русский

Специализация prod_bij с биекцией индексов e : ι → κ.

LaTeX

$$$\\forall e:\\, \\iota \\to \\kappa\\; (he: e.Bijective)\\; (hst : ∀ i, i ∈ s ↔ e i ∈ t)\\; (hfg : ∀ i ∈ s, f i = g (e i))\\; \\Rightarrow \\prod_{i ∈ s} f i = \\prod_{i ∈ t} g i$$$

Lean4

@[to_additive (attr := simp)]
theorem prod_ite_irrel (p : Prop) [Decidable p] (s : Finset ι) (f g : ι → M) :
    ∏ x ∈ s, (if p then f x else g x) = if p then ∏ x ∈ s, f x else ∏ x ∈ s, g x := by split_ifs with h <;> rfl

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