isClosed_iff_close_eq_self — Mathlib

English

Let S be a sieve on an object X in a Grothendieck topology J. Then S is closed with respect to J if and only if its closure with respect to J equals S.

Русский

Пусть S — расселе́ние на объекте X в топологии Гротендика J. Тогда S замкнуто относительно J тогда и только тогда, когда его замыкание относительно J равно S.

LaTeX

$$$J_1\\text{.IsClosed}(S) \\iff J_1\\text{.close}(S) = S$$$

Lean4

/-- The sieve `S` is closed iff its closure is equal to itself. -/
theorem isClosed_iff_close_eq_self {X : C} (S : Sieve X) : J₁.IsClosed S ↔ J₁.close S = S :=
  (J₁.closureOperator _).isClosed_iff

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