closure_closure — Mathlib

English

The closure operator is idempotent: closure(closure(X)) = closure(X).

Русский

Замыкание идемпотентно: cl(cl(X)) = cl(X).

LaTeX

$$$ M.\\mathrm{closure}(M.\\mathrm{closure}(X)) = M.\\mathrm{closure}(X) $$$

Lean4

@[simp]
theorem closure_closure (M : Matroid α) (X : Set α) : M.closure (M.closure X) = M.closure X :=
  (M.subset_closure _).antisymm'
    (subset_sInter (fun F hF ↦ (closure_subset_closure _ (sInter_subset_of_mem hF)).trans hF.1.closure.subset))

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