closure_insert_closure_eq_closure_insert

English

For any e and X, cl(insert e (cl X)) = cl(insert e X).

Русский

Для любого элемента e и множества X выполнено cl(insert e (cl X)) = cl(insert e X).

LaTeX

$$$\\operatorname{cl}(\\operatorname{insert} \\\\_{e}(\\operatorname{cl}(X))) = \\operatorname{cl}(\\operatorname{insert} \\\\_{e}X)$$$

Lean4

@[simp]
theorem closure_insert_closure_eq_closure_insert (M : Matroid α) (e : α) (X : Set α) :
    M.closure (insert e (M.closure X)) = M.closure (insert e X) := by
  simp_rw [← singleton_union, closure_union_closure_right_eq]

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