app_comp_p

Mathlib.CategoryTheory.Idempotents.FunctorCategories

URI: https://scilib.ai/kg/mathlib#CategoryTheory.Idempotents.app_comp_p

English

For any f: P ⟶ Q and X, P.p.app X ∘ f.f.app X = f.f.app X ∘ Q.p.app X.

Русский

Для любого f: P ⟶ Q и любого X выполняется P.p.app X ∘ f.f.app X = f.f.app X ∘ Q.p.app X.

LaTeX

$$P.p.app X \\circ f.f.app X = f.f.app X \\circ Q.p.app X$$

Lean4

@[reassoc (attr := simp)]
theorem app_comp_p : f.f.app X ≫ Q.p.app X = f.f.app X :=
  congr_app (comp_p f) X

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

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

Разделы

Аффилиация

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