Theorems · Theorem · combinatorics

Finset.sigma_preimage_mk

∀ {α : Type u} {β : α → Type u_1} [inst : DecidableEq α] (s : Finset ((a : α) × β a)) (t : Finset α),
  (t.sigma fun a => s.preimage (Sigma.mk a) ⋯) = {a ∈ s | a.fst ∈ t}

Defined in

Mathlib.Data.Finset.Preimage

Cited by

3 results in Mathlib

Foundations

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

Assumes

DecidableEq