prod_attach_univ — Mathlib

English

For a finite type ι, and a function f on the subtype {i ∈ univ} to M, the product over univ.attach equals the product over univ with the canonical embedding: ∏ i∈univ.attach, f i = ∏ i, f ⟨i, mem_univ i⟩.

Русский

Для конечного ι и функции f на подтипе {i ∈ унив}. произведение по univ.attach равно произведению по univ через каноническое вложение: ∏ i∈univ.attach, f i = ∏ i, f ⟨i, mem_univ i⟩.

LaTeX

$$$$\prod_{i \in \mathrm{univ}.\mathrm{attach}} f(i) = \prod_{i} f\langle i, \mathrm{mem\_univ}(i)\rangle.$$$$

Lean4

@[to_additive (attr := simp)]
theorem prod_attach_univ [Fintype ι] (f : { i // i ∈ @univ ι _ } → M) :
    ∏ i ∈ univ.attach, f i = ∏ i, f ⟨i, mem_univ _⟩ :=
  Fintype.prod_equiv (Equiv.subtypeUnivEquiv mem_univ) _ _ <| by simp

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