tprod_of_add_one_of_neg_add_one — Mathlib

English

Same as Split Multipliable for a variant with a T2 space, reaffirming the product decomposition over a subset and its complement.

Русский

То же самое, что и разложение произведения на подмножество и дополняющее множество, но в контексте пространства T2.

LaTeX

$$$$\\left(\\prod' x : s, f x\\right) \\cdot \\prod' x : \\uparrow s^c, f x = \\prod' x, f x.$$$$

Lean4

@[to_additive tsum_of_add_one_of_neg_add_one]
theorem tprod_of_add_one_of_neg_add_one [T2Space M] {f : ℤ → M} (hf₁ : Multipliable fun n : ℕ ↦ f (n + 1))
    (hf₂ : Multipliable fun n : ℕ ↦ f (-(n + 1))) :
    ∏' n : ℤ, f n = (∏' n : ℕ, f (n + 1)) * f 0 * ∏' n : ℕ, f (-(n + 1)) :=
  (hf₁.hasProd.of_add_one_of_neg_add_one hf₂.hasProd).tprod_eq

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