instFunctor

Mathlib.Data.Set.Defs

URI: https://scilib.ai/kg/mathlib#Set.instFunctor

English

There is a functor structure on Set, with map defined by the image operation: map f = image f.

Русский

На множество Set задана структура функторности, где отображение map определяется как образ функции: map f = image f.

LaTeX

$$$\text{Set}$ is a functor with \ map(f) = \text{image}(f).$$

Lean4

instance : Functor Set where map := @Set.image

Похожие утверждения

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru