subpresheafToTypes

Mathlib.Topology.Sheaves.LocalPredicate

URI: https://scilib.ai/kg/mathlib#TopCat.subpresheafToTypes

Lean4

/-- The subpresheaf of dependent functions on `X` satisfying the "pre-local" predicate `P`.
-/
@[simps!]
def subpresheafToTypes (P : PrelocalPredicate T) : Presheaf (Type _) X
    where
  obj U := { f : ∀ x : U.unop, T x // P.pred f }
  map {_ _} i f := ⟨fun x ↦ f.1 (i.unop x), P.res i.unop f.1 f.2⟩

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

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

Разделы

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

Аффилиация

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