Theorems · Definition

Set.image

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

The image of s : Set α by f : α → β, written f '' s, is the set of b : β such that f a = b for some a ∈ s.

Defined in

Mathlib.Data.Set.Defs

Cited by

5,609 results in Mathlib

Foundations

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