cRk — Mathlib

English

The rank of X in M, denoted cRk, is defined as the cRank of the restricted matroid M|X.

Русский

Ранг X в M, обозначаемый cRk, определяется как cRank ограниченного матроида M|X.

LaTeX

$$$\\mathrm{cRk}(M,X) = (M\\restriction X).\\mathrm{cRank}$$$

Lean4

/-- The rank (supremum of the cardinalities of bases) of a set `X` in a matroid `M`,
as a `Cardinal`. See `Matroid.eRk` for a better-behaved `ℕ∞`-valued version. -/
noncomputable def cRk (M : Matroid α) (X : Set α) :=
  (M ↾ X).cRank

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