Theorems · Definition

Function.swap

{α : Sort u₁} → {β : Sort u₂} → {φ : α → β → Sort u₃} → ((x : α) → (y : β) → φ x y) → (y : β) → (x : α) → φ x y

For a two-argument function f, swap f is the same function but taking the arguments in the reverse order. swap f y x = f x y.

Defined in

Mathlib.Logic.Function.Defs

Cited by

216 results in Mathlib

Foundations

Depth 0 from the axioms, rests on 1 definitions · uses no axioms