prod_subtype_eq_prod_filter — Mathlib

English

A product over a subtype defined by a predicate equals the product over the original set filtered by that predicate.

Русский

Произведение по подмножеству, заданному предикатом, равно произведению по исходному множеству, отфильтрованному по этому предикату.

LaTeX

$$$\prod x\in s.subtype p, f x = \prod x\in s with p x, f x$$$

Lean4

/-- A product over `s.subtype p` equals one over `{x ∈ s | p x}`. -/
@[to_additive (attr := simp) /-- A sum over `s.subtype p` equals one over `{x ∈ s | p x}`. -/
    ]
theorem prod_subtype_eq_prod_filter (f : ι → M) {p : ι → Prop} [DecidablePred p] :
    ∏ x ∈ s.subtype p, f x = ∏ x ∈ s with p x, f x :=
  by
  have := prod_map (s.subtype p) (Function.Embedding.subtype _) f
  simp_all

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