homToIndex

Mathlib.Topology.Sheaves.SheafCondition.OpensLeCover

URI: https://scilib.ai/kg/mathlib#TopCat.Presheaf.SheafCondition.OpensLeCover.homToIndex

English

There is a canonical morphism from V to U(index V) in Opens.

Русский

Существует каноническое отображение из V в U(индекс(V)) в Opens.

LaTeX

$$$\mathrm{homToIndex}(V): V.obj \to U(\mathrm{index}(V)).$$$

Lean4

/-- The morphism from `V` to `U i` for some `i`.
-/
def homToIndex (V : OpensLeCover U) : V.obj ⟶ U (index V) :=
  V.property.choose_spec.hom

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

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

Разделы

Аффилиация

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