tprod_fiberwise — Mathlib

English

The total product over a pair equals the product over the base and the fiber: tprod over p of f p equals tprod over b and c of f ⟨b,c⟩, when f is Multipliable.

Русский

Суммарное (полное) произведение по паре p равно произведению по основанию и волокну, если f совмножима.

LaTeX

$$$\\operatorname{tprod} f = \\operatorname{tprod} (b => \\operatorname{tprod} (c => f(\\langle b,c\\rangle)))$$$

Lean4

@[to_additive]
theorem tprod_fiberwise [T2Space α] {f : β → α} {a : α} (hf : HasProd f a) (g : β → γ) :
    HasProd (fun c : γ ↦ ∏' b : g ⁻¹' { c }, f b) a :=
  (((Equiv.sigmaFiberEquiv g).hasProd_iff).mpr hf).sigma <| fun _ ↦ ((hf.multipliable.subtype _).hasProd_iff).mpr rfl

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