Theorems · Definition · logic and foundations

Set.MapsTo.restrict

{α : Type u} → {β : Type v} → (f : α → β) → (s : Set α) → (t : Set β) → Set.MapsTo f s t → ↑s → ↑t

Given a map f sending s : Set α into t : Set β, restrict domain of f to s and the codomain to t. Same as Subtype.map.

Defined in

Mathlib.Data.Set.Operations

Cited by

57 results in Mathlib

Foundations

Depth 6 from the axioms · uses no axioms