eRk_insert_closure_eq — Mathlib

English

For any element e and set X, eRk(insert e (closure X)) = eRk(insert e X).

Русский

Для любого элемента e и множества X: eRk(⊔e (closure X)) = eRk(⊔e X).

LaTeX

$$$ M.eRk(\\{e\\} \\cup M.closure X) = M.eRk(\\{e\\} \\cup X) $$$

Lean4

@[simp]
theorem eRk_insert_closure_eq (M : Matroid α) (e : α) (X : Set α) :
    M.eRk (insert e (M.closure X)) = M.eRk (insert e X) := by
  rw [← union_singleton, eRk_union_closure_left_eq, union_singleton]

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