postcomp_iff

Mathlib.CategoryTheory.MorphismProperty.Composition

URI: https://scilib.ai/kg/mathlib#CategoryTheory.MorphismProperty.postcomp_iff

← MathLib Explorer

English

Under suitable RespectsRight and HasOfPostcompProperty assumptions, W(f ≫ g) holds iff W f.

Русский

При подходящих допущениях W (f ≫ g) эквивалентно W f.

LaTeX

$$$W(f \gg g) \iff W f$$$

Lean4

theorem postcomp_iff [W.RespectsRight W'] [W.HasOfPostcompProperty W'] {X Y Z : C} (f : X ⟶ Y) (g : Y ⟶ Z) (hg : W' g) :
    W (f ≫ g) ↔ W f :=
  ⟨W.of_postcomp f g hg, fun hf ↦ RespectsRight.postcomp _ hg _ hf⟩

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

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

Разделы

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

Аффилиация

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