costar_comp

Mathlib.Combinatorics.Quiver.Covering

URI: https://scilib.ai/kg/mathlib#Prefunctor.costar_comp

Lean4

theorem costar_comp (u : U) : (φ ⋙q ψ).costar u = ψ.costar (φ.obj u) ∘ φ.costar u :=
  rfl

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

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

Разделы

Аффилиация

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