tprod_setProd_singleton_left — Mathlib

English

Let b ∈ β, t ⊆ γ. The tprod over x in {b} ×ˢ t of f x equals the tprod over c ∈ t of f(b, c).

Русский

Пусть b ∈ β, t ⊆ γ. Т-продукт по x ∈ {b} ×ˢ t f x равен т-продукту по c ∈ t f(b, c).

LaTeX

$$$\\left( \\prod' x : \\{ b \\} \\timesˢ t, f x \\right) = \\prod' c : t, f (b, c)$$$

Lean4

@[to_additive tsum_setProd_singleton_left]
theorem tprod_setProd_singleton_left (b : β) (t : Set γ) (f : β × γ → α) :
    (∏' x : { b } ×ˢ t, f x) = ∏' c : t, f (b, c) := by
  rw [tprod_congr_set_coe _ Set.singleton_prod, tprod_image _ (Prod.mk_right_injective b).injOn]

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