mem_sieves_iff_coe

Mathlib.CategoryTheory.Sites.Grothendieck

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

English

For any object X and sieve S on X, S belongs to J.sieves X if and only if S belongs to J X.

Русский

Пусть X — объект и S — решёт на X. Тогда S принадлежит J.sieves X тогда и только тогда, когда S принадлежит J X.

LaTeX

$$S ∈ J.sieves X ⇔ S ∈ J X$$

Lean4

@[simp]
theorem mem_sieves_iff_coe : S ∈ J.sieves X ↔ S ∈ J X :=
  Iff.rfl

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

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

Разделы

Аффилиация

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