instNonempty

Mathlib.CategoryTheory.Sites.Hypercover.One

URI: https://scilib.ai/kg/mathlib#CategoryTheory.GrothendieckTopology.OneHypercover.instNonempty

English

For any object S, there exists at least one OneHypercover of S (the trivial one).

Русский

Для любого объекта S существует как минимум одно 1-гиперпокрытие S (тривиальное).

LaTeX

$$$\mathrm{Nonempty} (J.OneHypercover S)$$$

Lean4

instance (S : C) : Nonempty (J.OneHypercover S) :=
  ⟨trivial J S⟩

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

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

Разделы

Аффилиация

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