sigma_factor — Mathlib

English

If HasProd f a and g is any map, then the fiberwise tprod along the preimages defined by g yields HasProd: HasProd (λ c, ∏' b ∈ g⁻¹{c}, f b) a.

Русский

Пусть HasProd f a, тогда по любому отображению g возникает разбор по волокнам: HasProd (λ c, ∏' b ∈ g⁻¹{c}, f b) a.

LaTeX

$$$$ \\text{If } \\mathrm{HasProd}(f,a) , \\text{ then } \\mathrm{HasProd}(\\lambda c, \\prod' b\\in g^{-1}\\{c\\}, f\,b)\\, a. $$$$

Lean4

@[to_additive]
theorem sigma_factor {γ : β → Type*} {f : (Σ b : β, γ b) → α} (ha : Multipliable f) (b : β) :
    Multipliable fun c ↦ f ⟨b, c⟩ :=
  ha.comp_injective sigma_mk_injective

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