restrict_rankFinite — Mathlib

English

Restriction preserves finite rank: if M has finite rank, then the restricted matroid M|R also has finite rank.

Русский

Ограничение сохраняет конечный ранг: если ранг M конечен, то и ограничение M до R имеет конечный ранг.

LaTeX

$$$ (M|R).RankFinite $$$

Lean4

instance restrict_rankFinite [M.RankFinite] (R : Set α) : (M ↾ R).RankFinite :=
  let ⟨_, hB⟩ := (M ↾ R).exists_isBase
  hB.rankFinite_of_finite (hB.indep.of_restrict.finite)

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