isRkFinite_iff_finite

Mathlib.Combinatorics.Matroid.Rank.Finite

URI: https://scilib.ai/kg/mathlib#Matroid.Indep.isRkFinite_iff_finite

English

For an independent set I, I has finite rank iff I is finite.

Русский

Для независимого множества I ранг I конечен тогда и только тогда, когда I конечно.

LaTeX

$$$ M.Indep(I) \\rightarrow I \\text{finite} \\Leftrightarrow M.IsRkFinite(I) $$$

Lean4

theorem isRkFinite_iff_finite (hI : M.Indep I) : M.IsRkFinite I ↔ I.Finite :=
  hI.isBasis_self.finite_iff_isRkFinite.symm

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

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

Разделы

Аффилиация

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