toENat_cRank_eq — Mathlib

English

For any matroid M, (M.cRank).toENat = M.eRank.

Русский

Для любого матроида M, (cRank(M)).toENat равно eRank(M).

LaTeX

$$$ M.cRank.toENat = M.eRank $$$

Lean4

@[simp]
theorem toENat_cRank_eq (M : Matroid α) : M.cRank.toENat = M.eRank :=
  by
  obtain h | h := M.rankFinite_or_rankInfinite
  · obtain ⟨B, hB⟩ := M.exists_isBase
    rw [← hB.cardinalMk_eq_cRank, ← hB.encard_eq_eRank, toENat_cardinalMk]
  simp [rankInfinite_iff_aleph0_le_cRank.1 h]

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