eRk — Mathlib

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

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