close_close — Mathlib

English

Closure is idempotent: applying closure to a closed sieve S yields the same closure as applying closure once.

Русский

Замыкание идемпотентно: применение замыкания к замкнутому сайву S даёт тот же результат, что и однократное замыкание.

LaTeX

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

Lean4

@[simp]
theorem close_close {X : C} (S : Sieve X) : J₁.close (J₁.close S) = J₁.close S :=
  (J₁.closureOperator _).idempotent _

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