IsRkFinite — Mathlib

English

IsRkFinite M X is defined as (M ⧸ X).RankFinite; i.e., X has finite rank in M if and only if the restriction M|X has finite rank.

Русский

IsRkFinite M X определяется как (M|X).RankFinite; то есть ранг X в M конечен тогда и только тогда, когда ограничение M|X имеет конечный ранг.

LaTeX

$$$ \\mathrm{IsRkFinite}(M,X) := (M \\upharpoonright X).\\mathrm{RankFinite} $$$

Lean4

/-- `Matroid.IsRkFinite M X` means that every basis of `X` in `M` is finite. -/
def IsRkFinite (M : Matroid α) (X : Set α) : Prop :=
  (M ↾ X).RankFinite

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