English
The rank eRk of a set X in M is defined as the ENat-valued rank of the restriction M|_X.
Русский
Ранг eRk множества X в M определяется как ENat-значный ранг ограниченного матроида M|_X.
LaTeX
$$$ \\mathrm{eRk}(M,X) := (M \\restriction X).\\mathrm{eRank} $$$
Lean4
/-- The rank `Matroid.eRk M X` of a set `X` is the `ℕ∞`-valued cardinality of each basis of `X`.
(See `Matroid.cRk` for a worse-behaved cardinal-valued version) -/
noncomputable def eRk (M : Matroid α) (X : Set α) : ℕ∞ :=
(M ↾ X).eRank