Theorems · Theorem · combinatorics

Fintype.piFinset_image

∀ {α : Type u_1} [inst : DecidableEq α] [inst_1 : Fintype α] {γ : α → Type u_3} {δ : α → Type u_4}
  [inst_2 : (a : α) → DecidableEq (δ a)] (f : (a : α) → γ a → δ a) (s : (a : α) → Finset (γ a)),
  (Fintype.piFinset fun a => Finset.image (f a) (s a)) = Finset.image (fun b a => f a (b a)) (Fintype.piFinset s)

Defined in

Mathlib.Data.Fintype.Pi

Cited by

4 results in Mathlib

Foundations

Depth 76 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

DecidableEqFintypeDecidableEq