trivial_covering

Mathlib.CategoryTheory.Sites.Grothendieck

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

English

In the trivial Grothendieck topology, a sieve S on X belongs to the topology if and only if S = ⊤.

Русский

В тривиальной топологии Гротендик решётка S принадлежит топологии тогда и только тогда, когда S = ⊤.

LaTeX

$$S ∈ trivial C X ⇔ S = ⊤$$

Lean4

theorem trivial_covering : S ∈ trivial C X ↔ S = ⊤ :=
  Set.mem_singleton_iff

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

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

Разделы

Аффилиация

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