closure_closure_union_closure_eq_closure_union

English

For any X, Y, the closure of the union of their closures equals the closure of their union.

Русский

Для любых X, Y: cl(cl(X) ∪ cl(Y)) = cl(X ∪ Y).

LaTeX

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

Lean4

theorem closure_closure_union_closure_eq_closure_union (M : Matroid α) (X Y : Set α) :
    M.closure (M.closure X ∪ M.closure Y) = M.closure (X ∪ Y) :=
  by
  rw [eq_comm, union_eq_iUnion, ← closure_iUnion_closure_eq_closure_iUnion, union_eq_iUnion]
  simp_rw [Bool.cond_eq_ite, apply_ite]

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