instLawfulFunctor

Mathlib.Order.Filter.Map

URI: https://scilib.ai/kg/mathlib#Filter.instLawfulFunctor

English

Filter forms a lawful functor with respect to the map operation.

Русский

Фильтр образует законного функторa относительно операции отображения.

LaTeX

$$LawfulFunctor Filter$$

Lean4

instance : LawfulFunctor (Filter : Type u → Type u)
    where
  id_map _ := map_id
  comp_map _ _ _ := map_map.symm
  map_const := rfl

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

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

Разделы

Аффилиация

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