presheafToTop_obj — Mathlib

English

The presheaf toTop on a space X with fixed fiber T assigns to an open U the set of continuous maps from the subspace U (with the subspace topology) to T.

Русский

Прешеф к топологии (presheafToTop) на пространстве X задаёт для открытого множества U множество непрерывных отображений из подпространства U в T.

LaTeX

$$$(\\mathrm{presheafToTop}\\ X\\ T).obj U = ((\\mathrm{Opens.toTopCat}\\ X).obj (unop U) \\to T)$$$

Lean4

@[simp]
theorem presheafToTop_obj (T : TopCat) (U : (Opens X)ᵒᵖ) :
    (presheafToTop X T).obj U = ((Opens.toTopCat X).obj (unop U) ⟶ T) :=
  rfl

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