sieves_copy

Mathlib.CategoryTheory.Sites.Grothendieck

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

English

The sieves field of a copied topology is exactly the given sieve family: (J.copy s h).sieves = s.

Русский

Поле решёток скопированной топологии точно равно данному семейству решёток: (J.copy s h).sieves = s.

LaTeX

$$(J.copy\, s\, h).sieves = s$$

Lean4

@[simp]
theorem sieves_copy {J : GrothendieckTopology C} {s : ∀ X : C, Set (Sieve X)} {h : J.sieves = s} :
    (J.copy s h).sieves = s :=
  rfl

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

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

Разделы

Аффилиация

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