prod_mapRange_index — Mathlib

English

Given f: M → M', hf: f 0 = 0, g: α →₀ M, h: α → M' → N and h0: ∀ a, h a 0 = 1, one has (mapRange f hf g).prod h = g.prod (λ a b, h a (f b)).

Русский

Пусть f: M → M', hf: f 0 = 0, g: α →₀ M, h: α → M' → N и h0: ∀ a, h a 0 = 1. Тогда (mapRange f hf g).prod h = g.prod (λ a b, h a (f b)).

LaTeX

$$$ (mapRange f hf g).prod h = g.prod (fun a b => h a (f b)) $$$

Lean4

@[to_additive]
theorem prod_mapRange_index {f : M → M'} {hf : f 0 = 0} {g : α →₀ M} {h : α → M' → N} (h0 : ∀ a, h a 0 = 1) :
    (mapRange f hf g).prod h = g.prod fun a b => h a (f b) :=
  Finset.prod_subset support_mapRange fun _ _ H => by rw [notMem_support_iff.1 H, h0]

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