Theorems · Definition

Function.onFun

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

Given functions f : β → β → φ and g : α → β, produce a function α → α → φ that evaluates g on each argument, then applies f to the results. Can be used, e.g., to transfer a relation from β to α.

Defined in

Mathlib.Logic.Function.Defs

Cited by

570 results in Mathlib

Foundations

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