instFunctor — Mathlib

English

There is a Functor structure on Filter given by map, i.e., the Filter type is a functor with map defined by Filter.map.

Русский

Тип фильтров обладает структурой функторa: отображение по заданной функции задаёт морфизм между фильтрами, то есть Filter является функтором с map = Filter.map.

LaTeX

$$$\text{inst}\; \text{Functor}_{\mathrm{Filter}}:\; \mathrm{map} = \mathrm{Filter.map}. $$$

Lean4

instance : Functor Filter where map := @Filter.map

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