sigma_of_hasProd — Mathlib

English

If h1 gives fiberwise Multipliable and h2 gives whole f Multipliable, then tprod f equals tprod of inner tprod's.

Русский

Если h1 задаёт волокна как Multipliable, а h2 — целиком f Multipliable, то т-продукт равен т-продукту вложенных т-продуктов.

LaTeX

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

Lean4

@[to_additive]
theorem sigma_of_hasProd {γ : β → Type*} {f : (Σ b : β, γ b) → α} {g : β → α} {a : α} (ha : HasProd g a)
    (hf : ∀ b, HasProd (fun c ↦ f ⟨b, c⟩) (g b)) (hf' : Multipliable f) : HasProd f a := by
  simpa [(hf'.hasProd.sigma hf).unique ha] using hf'.hasProd

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