isRkFinite_of_finite

Mathlib.Combinatorics.Matroid.Rank.Finite

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

English

If hI is a finite basis' of X, then M.IsRkFinite X.

Русский

Если hI — конечный база'- X, то M.IsRkFinite X.

LaTeX

$$$ (hI : M.IsBasis' I X) \\land I.Finite \\Rightarrow M.IsRkFinite X $$$

Lean4

theorem isRkFinite_of_finite (hI : M.IsBasis' I X) (hIfin : I.Finite) : M.IsRkFinite X :=
  ⟨I, hI, hIfin⟩

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

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

Разделы

Аффилиация

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