tprod_sigma' — Mathlib

English

Same as 195435 but stated with minor simplification under regularity assumptions; equality between tprod of f and iterated tprod of fiberwise values.

Русский

То же, что и в 195435, но формулируется с небольшим упрощением под условием регулярности; равенство между т-продуктом f и вложенными т-продуктами по волокнам.

LaTeX

$$$(ha : Multipliable f) → (∀ b, Multipliable (λ c, f ⟨b,c⟩)) → Eq (tprod f) (tprod (λ b, tprod (λ c, f ⟨b,c⟩)))$$$

Lean4

@[to_additive]
protected theorem tprod_sigma' {γ : β → Type*} {f : (Σ b : β, γ b) → α} (h₁ : ∀ b, Multipliable fun c ↦ f ⟨b, c⟩)
    (h₂ : Multipliable f) : ∏' p, f p = ∏' (b) (c), f ⟨b, c⟩ :=
  (h₂.hasProd.sigma fun b ↦ (h₁ b).hasProd).tprod_eq.symm

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