eRank_freeOn — Mathlib

English

For any X, the eRank of the free matroid on X equals the encard of X: (freeOn X).eRank = X.encard.

Русский

Для любого множества X eRank свободного матроида на X равен encard(X): (freeOn X).eRank = X.encard.

LaTeX

$$$ (\\mathrm{freeOn}~X).eRank = X.encard $$$

Lean4

@[simp]
theorem eRank_freeOn (X : Set α) : (freeOn X).eRank = X.encard := by
  rw [eRank_def, freeOn_ground, (freeOn_indep_iff.2 rfl.subset).eRk_eq_encard]

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