Theorems · Definition

Pi.map

{ι : Sort u_1} → {α : ι → Sort u_2} → {β : ι → Sort u_3} → ((i : ι) → α i → β i) → ((i : ι) → α i) → (i : ι) → β i

Sends a dependent function a : ∀ i, α i to a dependent function Pi.map f a : ∀ i, β i by applying f i to i-th component.

Defined in

Mathlib.Logic.Function.Defs

Cited by

60 results in Mathlib

Foundations

Depth 0 from the axioms · uses no axioms