Theorems · Definition · logic and foundations

Set.image2

{α : Type u} → {β : Type v} → {γ : Type w} → (α → β → γ) → Set α → Set β → Set γ

The image of a binary function f : α → β → γ as a function Set α → Set β → Set γ. Mathematically this should be thought of as the image of the corresponding function α × β → γ.

Defined in

Mathlib.Data.Set.Operations

Cited by

311 results in Mathlib

Foundations

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