indexOfHom_spec

Mathlib.Topology.Sheaves.SheafCondition.Sites

URI: https://scilib.ai/kg/mathlib#TopCat.Presheaf.presieveOfCovering.indexOfHom_spec

English

The covering obtained from presieveOfCovering U yields a covering of iSup U in the Grothendieck topology.

Русский

Покрытие, полученное из presieveOfCovering U, покрывает iSup U в GrothendieckTopology.

LaTeX

$$$\\text{coveringOfPresieve}$$$

Lean4

theorem indexOfHom_spec (f : Σ V, { f : V ⟶ iSup U // presieveOfCovering U f }) : f.1 = U (indexOfHom U f) :=
  f.2.2.choose_spec

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

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

Разделы

Аффилиация

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