prod_fiberwise_eq_prod_filter' — Mathlib

English

A variant where the inner index is permuted to align with the outer fiber index, giving an equality with inner terms replaced by f(g(i)).

Русский

Вариант, где внутренний индекс приведён к соответствующему волокну внешнего индекса и правая часть выражения заменена на f(g(i)).

LaTeX

$$$\prod_{j\in t} \prod_{i\in s with\ g(i)=j} f(j) = \prod_{i\in s with\ g(i)\in t} f(g(i))$$$

Lean4

@[to_additive]
theorem prod_fiberwise_eq_prod_filter' (s : Finset ι) (t : Finset κ) (g : ι → κ) (f : κ → M) :
    ∏ j ∈ t, ∏ i ∈ s with g i = j, f j = ∏ i ∈ s with g i ∈ t, f (g i) := by
  calc
    _ = ∏ j ∈ t, ∏ i ∈ s with g i = j, f (g i) :=
      prod_congr rfl fun j _ ↦ prod_congr rfl fun i hi ↦ by rw [(mem_filter.1 hi).2]
    _ = _ := prod_fiberwise_eq_prod_filter _ _ _ _

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