# Documentation

Mathlib.Data.Set.Functor

# Functoriality of Set#

This file defines the functor structure of Set.

f <$> s = f '' s @[simp] theorem Set.seq_eq_set_seq {α : Type u} {β : Type u} (s : Set (αβ)) (t : Set α) : (Seq.seq s fun x => t) = Set.seq s t @[simp] theorem Set.pure_def {α : Type u} (a : α) : pure a = {a} theorem Set.image2_def {α : Type u_1} {β : Type u_1} {γ : Type u_1} (f : αβγ) (s : Set α) (t : Set β) : Set.image2 f s t = Seq.seq (f <$> s) fun x => t
Set.image2 in terms of monadic operations. Note that this can't be taken as the definition because of the lack of universe polymorphism.