Theorems · Theorem · combinatorics

Fintype.mem_piFinset

∀ {α : Type u_1} [inst : DecidableEq α] [inst_1 : Fintype α] {δ : α → Type u_4} {t : (a : α) → Finset (δ a)}
  {f : (a : α) → δ a}, f ∈ Fintype.piFinset t ↔ ∀ (a : α), f a ∈ t a

Defined in

Mathlib.Data.Fintype.Pi

Cited by

9 results in Mathlib

Foundations

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

Assumes

DecidableEqFintype