tprod_setProd_singleton_right — Mathlib

English

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

Русский

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

LaTeX

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

Lean4

@[to_additive tsum_setProd_singleton_right]
theorem tprod_setProd_singleton_right (s : Set β) (c : γ) (f : β × γ → α) :
    (∏' x : s ×ˢ { c }, f x) = ∏' b : s, f (b, c) := by
  rw [tprod_congr_set_coe _ Set.prod_singleton, tprod_image _ (Prod.mk_left_injective c).injOn]

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