pushforwardFamily_def

Mathlib.CategoryTheory.Sites.DenseSubsite.Basic

URI: https://scilib.ai/kg/mathlib#CategoryTheory.Functor.IsCoverDense.Types.pushforwardFamily_def

Lean4

@[simp]
theorem pushforwardFamily_def {X} (x : ℱ.obj (op X)) :
    pushforwardFamily α x = fun _ _ hf => ℱ'.val.map hf.some.lift.op <| α.app (op _) (ℱ.map hf.some.map.op x) :=
  rfl

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

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

Разделы

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

Аффилиация

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