Theorems · Inductive type

Function.HasUncurry

Type u_5 → outParam (Type u_6) → outParam (Type u_7) → Type (max (max u_5 u_6) u_7)

Records a way to turn an element of α into a function from β to γ. The most generic use is to recursively uncurry. For instance f : α → β → γ → δ will be turned into ↿f : α × β × γ → δ. One can also add instances for bundled maps.

Defined in

Mathlib.Logic.Function.Basic

Cited by

0 results in Mathlib

Foundations

Depth 1 from the axioms · uses no axioms