isRkFinite_of_finite

Mathlib.Combinatorics.Matroid.Rank.Finite

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

← MathLib Explorer

English

If X is finite, then M.IsRkFinite X holds.

Русский

Если X конечное, то M.IsRkFinite X верно.

LaTeX

$$$ X.Finite \\rightarrow M.IsRkFinite X $$$

Lean4

@[simp]
theorem isRkFinite_of_finite (M : Matroid α) (hX : X.Finite) : M.IsRkFinite X :=
  let ⟨_, hI⟩ := M.exists_isBasis' X
  hI.isRkFinite_of_finite (hX.subset hI.subset)

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

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

Разделы

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

Аффилиация

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