finite_of_isBasis

Mathlib.Combinatorics.Matroid.Rank.Finite

URI: https://scilib.ai/kg/mathlib#Matroid.IsRkFinite.finite_of_isBasis

English

An IsRkFinite X matroid has a finite basis' I with M.IsBasis' I X and I.Finite.

Русский

У матроидa IsRkFinite X существует конечная база I, такая что M.IsBasis' I X и I.Finite.

LaTeX

$$$ \\exists I, M.IsBasis' I X \\land I.Finite $$$

Lean4

theorem finite_of_isBasis (h : M.IsRkFinite X) (hI : M.IsBasis I X) : I.Finite :=
  h.finite_of_isBasis' hI.isBasis'

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

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

Разделы

Аффилиация

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