tprod_subtype_mul_tprod_subtype_compl

English

Let f be Multipliable. For any subset s, the infinite product over s, multiplied by the infinite product over the complement of s, equals the infinite product over all β.

Русский

Пусть f суммируема; для любого подмножества s бесконечный произведение по s, умноженное на бесконечное произведение по дополнению s, равно бесконечному произведению по всем β.

LaTeX

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

Lean4

@[to_additive]
protected theorem tprod_subtype_mul_tprod_subtype_compl [T2Space α] {f : β → α} (hf : Multipliable f) (s : Set β) :
    (∏' x : s, f x) * ∏' x : ↑sᶜ, f x = ∏' x, f x :=
  ((hf.subtype s).hasProd.mul_compl (hf.subtype {x | x ∉ s}).hasProd).unique hf.hasProd

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