Theorems · Theorem · combinatorics

Finset.mem_pi

∀ {α : Type u_1} {β : α → Type u} [inst : DecidableEq α] {s : Finset α} {t : (a : α) → Finset (β a)}
  {f : (a : α) → a ∈ s → β a}, f ∈ s.pi t ↔ ∀ (a : α) (h : a ∈ s), f a h ∈ t a

Defined in

Mathlib.Data.Finset.Pi

Cited by

5 results in Mathlib

Foundations

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

Assumes

DecidableEq