presheafToType_obj

Mathlib.Topology.Sheaves.PresheafOfFunctions

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

English

For the presheaf to type construction, the value on an open U is the set of all functions U.unop → T.

Русский

Для конструкция presheafToType значение на открытом U равно множеству функций U.unop → T.

LaTeX

$$$(\\mathrm{presheafToType}\\ X\\ T).obj U = U.unop \\to T$$$

Lean4

@[simp]
theorem presheafToType_obj {T : Type*} {U : (Opens X)ᵒᵖ} : (presheafToType X T).obj U = (U.unop → T) :=
  rfl

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

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

Разделы

Аффилиация

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