tprod_subtype — Mathlib

English

For a finite set s ⊆ β and any f: β → α, the tprod over the subtype {x ∈ s} equals the finite product over s: ∏' x : {x ∈ s}, f x = ∏ x ∈ s, f x.

Русский

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

LaTeX

$$$\\\\prod' x : { x ∈ s }, f x = \\\\prod x ∈ s, f x$$$

Lean4

@[to_additive (attr := simp)]
theorem tprod_subtype (s : Finset β) (f : β → α) : ∏' x : { x // x ∈ s }, f x = ∏ x ∈ s, f x := by rw [← prod_attach];
  exact tprod_fintype _

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