instNonempty

Mathlib.CategoryTheory.Sites.Hypercover.One

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

English

There exists a nonempty PreOneHypercover instance.

Русский

Существует ненулевой инстанс PreOneHypercover.

LaTeX

$$$\\text{Nonempty}(\\text{PreOneHypercover})$$$

Lean4

instance : Nonempty (PreOneHypercover.{w} S) :=
  ⟨trivial S⟩

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

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

Разделы

Аффилиация

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