tprod_subtype' — Mathlib

English

For a finite set s ⊆ β, the tprod over the subtype s as a Set equals the finite product over s: ∏' x : (s : Set β), f x = ∏ x ∈ s, f x.

Русский

Для конечного множества s верно: т-произведение по подмножеству s как множество равно обычному произведению по s.

LaTeX

$$$\\\\prod' x : (s : Set β), f x = \\\\prod x ∈ s, f x$$$

Lean4

@[to_additive]
theorem tprod_subtype' (s : Finset β) (f : β → α) : ∏' x : (s : Set β), f x = ∏ x ∈ s, f x := by simp

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