prod_image' — Mathlib

English

Relates a fiberwise product after mapping to κ with an inner product against g.

Русский

Связь произведения по образу с внутренним произведением через g.

LaTeX

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

Lean4

@[to_additive]
theorem prod_image' [DecidableEq ι] {s : Finset κ} {g : κ → ι} (h : κ → M)
    (eq : ∀ i ∈ s, f (g i) = ∏ j ∈ s with g j = g i, h j) : ∏ a ∈ s.image g, f a = ∏ i ∈ s, h i :=
  calc
    ∏ a ∈ s.image g, f a = ∏ a ∈ s.image g, ∏ j ∈ s with g j = a, h j :=
      (prod_congr rfl) fun _a hx =>
        let ⟨i, his, hi⟩ := mem_image.1 hx
        hi ▸ eq i his
    _ = ∏ i ∈ s, h i := prod_fiberwise_of_maps_to (fun _ => mem_image_of_mem g) _

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