tprod_tprod_eq_mulSingle — Mathlib

English

Let f: β → γ → α, with a row and column finite support at b and c respectively, and all other entries equal to 1; then the full tprod equals f(b,c): ∏' (b') (c'), f(b') c' = f(b,c).

Русский

Пусть f: β → γ → α так, что только при b, c ненулевые значения, а остальные равны 1; тогда двустороннее т-произведение равно f(b,c).

LaTeX

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

Lean4

@[to_additive]
theorem tprod_tprod_eq_mulSingle (f : β → γ → α) (b : β) (c : γ) (hfb : ∀ b' ≠ b, f b' c = 1)
    (hfc : ∀ b', ∀ c' ≠ c, f b' c' = 1) : ∏' (b') (c'), f b' c' = f b c :=
  calc
    ∏' (b') (c'), f b' c' = ∏' b', f b' c := tprod_congr fun b' ↦ tprod_eq_mulSingle _ (hfc b')
    _ = f b c := tprod_eq_mulSingle _ hfb

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