prod_indicator_index_eq_prod_attach

English

Let s be a finite set, f : ∀ a ∈ s, M, h : α → M → N with h a 0 = 1. Then (indicator s f).prod h equals the product over x ∈ s.attach of h x.1 (f x.1 x.2).

Русский

Пусть s — конечное множество, f : ∀ a ∈ s, M, h : α → M → N с h a 0 = 1. Тогда (indicator s f).prod h равно произведению по x ∈ s.attach от h x.1 (f x.1 x.2).

LaTeX

$$$\big(\operatorname{indicator} s f\big).prod h = \prod_{x \in s.attach} h \; x.1 \big(f x.1 x.2\big).$$$

Lean4

@[to_additive (attr := simp)]
theorem prod_indicator_index_eq_prod_attach [Zero M] [CommMonoid N] {s : Finset α} (f : ∀ a ∈ s, M) {h : α → M → N}
    (h_zero : ∀ a ∈ s, h a 0 = 1) : (indicator s f).prod h = ∏ x ∈ s.attach, h ↑x (f x x.2) :=
  by
  rw [prod_of_support_subset _ (support_indicator_subset _ _) h h_zero, ← prod_attach]
  refine Finset.prod_congr rfl (fun _ _ => ?_)
  rw [indicator_of_mem]

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