prod_fiberwise_of_maps_to — Mathlib

English

Let s be a finite set and g: ι → κ. Then the product over fibers equals the product of the fiberwise products over i ∈ s of f(i).

Русский

Пусть s - конечное множество и g: ι → κ. Тогда произведение по волокнам равно произведению по образам внутри каждого i ∈ s.

LaTeX

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

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 i = ∏ i ∈ s, f i :=
  by
  rw [← prod_disjiUnion, disjiUnion_filter_eq_of_maps_to h]
  #adaptation_note /-- 2025-09-12 (kmill) copied from private lemma pairwiseDisjoint_fibers -/

  intro x' hx y' hy hne
  simp_rw [disjoint_left, mem_filter]; rintro i ⟨_, rfl⟩ ⟨_, rfl⟩; exact hne rfl

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