isRkFinite_set

Mathlib.Combinatorics.Matroid.Rank.Finite

URI: https://scilib.ai/kg/mathlib#Matroid.isRkFinite_set

← MathLib Explorer

English

If M has finite rank, then every subset X has finite rank in M.

Русский

Если у M конечный ранг, то каждое подмножество X имеет конечный ранг в M.

LaTeX

$$$ [\\operatorname{RankFinite}(M)] \\Rightarrow \\forall X, M.IsRkFinite X $$$

Lean4

theorem isRkFinite_set (M : Matroid α) [RankFinite M] (X : Set α) : M.IsRkFinite X :=
  let ⟨_, hI⟩ := M.exists_isBasis' X
  hI.isRkFinite_of_finite hI.indep.finite

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

Научная платформа российской исследовательской школы.

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru