lawfulFunctor

Mathlib.Control.Traversable.Equiv

URI: https://scilib.ai/kg/mathlib#Equiv.lawfulFunctor

Lean4

protected theorem lawfulFunctor : @LawfulFunctor _ (Equiv.functor eqv) :=
  -- Add the instance to the local context (since `Equiv.functor` is not an instance).
    -- Although it can be found by unification, Lean prefers to synthesize instances and
    -- then check that they are defeq to the instance found by unification.

  let _inst := Equiv.functor eqv
  { map_const := fun {_ _} => rfl
    id_map := Equiv.id_map eqv
    comp_map := Equiv.comp_map eqv }

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

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

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

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