sigma' — Mathlib

English

If f is Multipliable on (β) and g is Multipliable fiberwise, then the product over Σ b γ b of f equals the iterated product over b of the products over fiber γ b.

Русский

Если f выполнима на Σ σ и g — внутри-фибер, то произведение по Σ f соответствует итеративному произведению по b от произведений по волокнам γ b.

LaTeX

$$$\\forall γ, f : (Σ b, γ b) → α, (ha : Multipliable f) (hf : ∀ b, Multipliable (λ c, f ⟨b,c⟩)) : ∏' p, f p = ∏' b (\\prod' c, f ⟨b,c⟩)$$$

Lean4

@[to_additive]
theorem sigma' {γ : β → Type*} {f : (Σ b : β, γ b) → α} (ha : Multipliable f)
    (hf : ∀ b, Multipliable fun c ↦ f ⟨b, c⟩) : Multipliable fun b ↦ ∏' c, f ⟨b, c⟩ :=
  (ha.hasProd.sigma fun b ↦ (hf b).hasProd).multipliable

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