monotone_close

Mathlib.CategoryTheory.Sites.Closed

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

English

The closure operator is monotone: if S ⊆ T then close S ⊆ close T.

Русский

Замыкание монотонно: если S ⊆ T, то close S ⊆ close T.

LaTeX

$$If S ⊆ T then J_1.\\text{close}(S) ⊆ J_1.\\text{close}(T).$$

Lean4

@[mono]
theorem monotone_close {X : C} : Monotone (J₁.close : Sieve X → Sieve X) :=
  (J₁.closureOperator _).monotone

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

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

Разделы

Аффилиация

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