tprod_extend_one — Mathlib

English

If g is injective, then extending f along g with base 1 preserves the total product: the fiberwise product over y equals the product over x.

Русский

Если g инъективно, расширение f вдоль g с единичной базой сохраняет полный произведение: произведение по волокнам равно произведению по x.

LaTeX

$$$\\prod' y , \\mathrm{extend} (g,f,1)\\,y = \\prod' x , f\,x$$$

Lean4

@[to_additive (attr := simp)]
theorem tprod_extend_one {γ : Type*} {g : γ → β} (hg : Injective g) (f : γ → α) : ∏' y, extend g f 1 y = ∏' x, f x :=
  by
  have : mulSupport (extend g f 1) ⊆ Set.range g := mulSupport_subset_iff'.2 <| extend_apply' _ _
  simp_rw [← hg.tprod_eq this, hg.extend_apply]

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