Theorems · Definition · combinatorics

Finset.pi

{α : Type u_1} →
  {β : α → Type u} → [DecidableEq α] → (s : Finset α) → ((a : α) → Finset (β a)) → Finset ((a : α) → a ∈ s → β a)

Given a finset s of α and for all a : α a finset t a of β a, then one can define the finset s.pi t of all functions defined on elements of s taking values in t a for a ∈ s. Note that the elements of s.pi t are only partially defined, on s.

Defined in

Mathlib.Data.Finset.Pi

Cited by

23 results in Mathlib

Foundations

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

Assumes

DecidableEq