prod_fiberwise_of_maps_to' — Mathlib

English

A variant where the inner index ranges with g i = j and f is evaluated at g i.

Русский

Вариант, где внутренняя индексация идёт с учётом g(i)=j, а f оценивается в g(i).

LaTeX

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

Lean4

@[to_additive]
theorem prod_fiberwise_of_maps_to' {g : ι → κ} (h : ∀ i ∈ s, g i ∈ t) (f : κ → M) :
    ∏ j ∈ t, ∏ i ∈ s with g i = j, f j = ∏ i ∈ s, f (g i) := by
  calc
    _ = ∏ j ∈ t, ∏ i ∈ s with g i = j, f (g i) :=
      prod_congr rfl fun y _ ↦ prod_congr rfl fun x hx ↦ by rw [(mem_filter.1 hx).2]
    _ = _ := prod_fiberwise_of_maps_to h _

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