cRk_closure — Mathlib

English

The cardinal rank is unchanged when passing to the closure: cRk(closure X) = cRk(X).

Русский

Кардинальная ранга сохраняется при взятии замыкания: cRk(closure X) = cRk(X).

LaTeX

$$$cRk(\mathrm{cl}(X)) = cRk(X)$$$

Lean4

@[simp]
theorem cRk_closure (M : Matroid α) [InvariantCardinalRank M] (X : Set α) : M.cRk (M.closure X) = M.cRk X :=
  by
  obtain ⟨I, hI⟩ := M.exists_isBasis' X
  rw [← hI.isBasis_closure_right.cardinalMk_eq_cRk, ← hI.cardinalMk_eq_cRk]

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