subpresheafContinuousPrelocalIsoPresheafToTop

Mathlib.Topology.Sheaves.LocalPredicate

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

Lean4

/-- Some repackaging:
the presheaf of functions satisfying `continuousPrelocal` is just the same thing as
the presheaf of continuous functions.
-/
def subpresheafContinuousPrelocalIsoPresheafToTop {X : TopCat.{u}} (T : TopCat.{u}) :
    subpresheafToTypes (continuousPrelocal X T) ≅ presheafToTop X T :=
  NatIso.ofComponents fun X ↦
    { hom := by rintro ⟨f, c⟩; exact ofHom ⟨f, c⟩
      inv := by rintro ⟨f, c⟩; exact ⟨f, c⟩ }

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

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

Разделы

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

Аффилиация

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