finite_iff_isRkFinite

Mathlib.Combinatorics.Matroid.Rank.Finite

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

English

If I is a basis' of X, then I.Finite ↔ M.IsRkFinite X, equivalently: Iff I.Finite (M.IsRkFinite X).

Русский

Если I является базисом'-ом X, то I.Finite ↔ M.IsRkFinite X.

LaTeX

$$$ hI.IsBasis'.finite_iff_isRkFinite $$$

Lean4

theorem finite_iff_isRkFinite (hI : M.IsBasis I X) : I.Finite ↔ M.IsRkFinite X :=
  hI.isBasis'.finite_iff_isRkFinite

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

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

Разделы

Аффилиация

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