eRk_closure_eq — Mathlib

English

The extended rank is invariant under taking closure: eRk(closure X) = eRk(X).

Русский

Расширенный ранг не зависит от замыкания: eRk(closure X) = eRk(X).

LaTeX

$$$ M.eRk( M.closure X ) = M.eRk X $$$

Lean4

@[simp]
theorem eRk_closure_eq (M : Matroid α) (X : Set α) : M.eRk (M.closure X) = M.eRk X :=
  by
  obtain ⟨I, hI⟩ := M.exists_isBasis' X
  rw [← hI.closure_eq_closure, ← hI.indep.isBasis_closure.encard_eq_eRk, hI.encard_eq_eRk]

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