English
Let f,g: β → γ → α be functions; if f(b,c) = g(b,c) for all b,c, then the iterated tprod over b with inner tprod over c equals the corresponding tprod with g: ∏'_{L} b, ∏'_{M} c, f(b,c) = ∏'_{L} b, ∏'_{M} c, g(b,c).
Русский
Пусть f,g: β → γ → α — функции. Если для всех b,c выполняется f(b,c) = g(b,c), то двойное т-произведение равняется соответствующему для g: ∏'_{L} b, ∏'_{M} c, f(b,c) = ∏'_{L} b, ∏'_{M} c, g(b,c).
LaTeX
$$$\\\\prod'_{L} b \\, \\\\\\prod'_{M} c \\, f(b,c) = \\\\prod'_{L} b \\, \\\\\\prod'_{M} c \\, g(b,c)$$$
Lean4
@[to_additive]
theorem tprod_congr₂ {f g : β → γ → α} {M : SummationFilter γ} (hfg : ∀ b c, f b c = g b c) :
∏'[L] b, ∏'[M] c, f b c = ∏'[L] b, ∏'[M] c, g b c :=
tprod_congr fun b ↦ tprod_congr fun c ↦ hfg b c
