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