tprod_eq

Mathlib.Topology.Algebra.InfiniteSum.Basic

URI: https://scilib.ai/kg/mathlib#Equiv.tprod_eq

English

If e is an equivalence between γ and β, then ∏' c, f (e c) = ∏' b, f b for any f: β→α.

Русский

Если e — эквиваленция между γ и β, то т-произведение по f ∘ e равно т-произведению по f.

LaTeX

$$$\\\\prod' c, f(e(c)) = \\\\prod' b, f(b)$$$

Lean4

@[to_additive]
theorem tprod_eq (e : γ ≃ β) (f : β → α) : ∏' c, f (e c) = ∏' b, f b :=
  e.injective.tprod_eq <| by simp

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru