instIsGeneratedByOneHypercovers

Mathlib.CategoryTheory.Sites.Hypercover.IsSheaf

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

English

An instance statement that J is generated by one-hypercovers for Grothendieck Topology.

Русский

Утверждение инстанса: J порождается одной гипер-обложкой.

LaTeX

$$$ [IsGeneratedByOneHypercovers\\ J] \\Rightarrow \\text{le } S hS$$$

Lean4

instance : IsGeneratedByOneHypercovers.{max u v} J where le S hS := ⟨Cover.oneHypercover ⟨S, hS⟩, by simp, by simp⟩

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

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

Разделы

Аффилиация

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