close_eq_self_of_isClosed — Mathlib

English

If a sieve S is closed, then applying the closure operator to S leaves S unchanged: close S = S.

Русский

Если расселение S замкнутоe, то применение оператора замыкания к S не изменяет его: close S = S.

LaTeX

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

Lean4

theorem close_eq_self_of_isClosed {X : C} {S : Sieve X} (hS : J₁.IsClosed S) : J₁.close S = S :=
  (J₁.isClosed_iff_close_eq_self S).1 hS

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