tprod_congr_set_coe — Mathlib

English

If two sets s and t are equal, then the infinite product over s equals the infinite product over t for any function f.

Русский

Если множества s и t равны, то бесконечный произведение по s равно по t для любой функции f.

LaTeX

$$∏'[L] x : s, f x = ∏'[L] x : t, f x$$

Lean4

@[to_additive]
theorem tprod_congr_set_coe (f : β → α) {s t : Set β} (h : s = t) : ∏' x : s, f x = ∏' x : t, f x := by rw [h]

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