closure_union_closure_right_eq — Mathlib

English

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

Русский

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

LaTeX

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

Lean4

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

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