covering_iff_covers_id

Mathlib.CategoryTheory.Sites.Grothendieck

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

English

Same as above, but expressed in a simplified form for the given context.

Русский

То же самое, выраженное в упрощённой форме.

LaTeX

$$J.Covers S f ↔ S.pullback f ∈ J Y$$

Lean4

theorem covering_iff_covers_id (S : Sieve X) : S ∈ J X ↔ J.Covers S (𝟙 X) := by simp [covers_iff]

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

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

Разделы

Аффилиация

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