Theorems · Definition · logic and foundations

Set.pi

{ι : Type u_1} → {α : ι → Type u_2} → Set ι → ((i : ι) → Set (α i)) → Set ((i : ι) → α i)

Given an index set ι and a family of sets t : Π i, Set (α i), pi s t is the set of dependent functions f : Πa, π a such that f i belongs to t i whenever i ∈ s.

Defined in

Mathlib.Data.Set.Operations

Cited by

405 results in Mathlib

Foundations

Depth 4 from the axioms, rests on 8 definitions · uses no axioms