closure_union_closure_left_eq — Mathlib

English

For sets X, Y, the closure of the closure X union Y equals the closure of X union Y.

Русский

Для множеств X, Y: cl(cl(X) ∪ Y) = cl(X ∪ Y).

LaTeX

$$$\\operatorname{cl}(\\operatorname{cl}(X) \\cup Y) = \\operatorname{cl}(X \\cup Y)$$$

Lean4

@[simp]
theorem closure_union_closure_left_eq (M : Matroid α) (X Y : Set α) : M.closure (M.closure X ∪ Y) = M.closure (X ∪ Y) :=
  by
  rw [← closure_closure_union_closure_eq_closure_union, closure_closure, closure_closure_union_closure_eq_closure_union]

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