map_comp

Mathlib.CategoryTheory.Sites.IsSheafFor

URI: https://scilib.ai/kg/mathlib#CategoryTheory.Presieve.FamilyOfElements.map_comp

Lean4

@[simp]
theorem map_comp (x : FamilyOfElements P R) (f : P ⟶ Q) (g : Q ⟶ U) : (x.map f).map g = x.map (f ≫ g) := by rfl

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

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

Разделы

Аффилиация

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