restrict_map

Mathlib.CategoryTheory.Sites.IsSheafFor

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

Lean4

theorem restrict_map (p : FamilyOfElements P R) (φ : P ⟶ Q) {R' : Presieve X} (h : R' ≤ R) :
    (p.restrict h).map φ = (p.map φ).restrict h :=
  rfl

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

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

Разделы

Аффилиация

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