cardinalMk_eq

Mathlib.Combinatorics.Matroid.Rank.Cardinal

URI: https://scilib.ai/kg/mathlib#Matroid.IsBase.cardinalMk_eq

English

If B and B' are bases of M, then |B| = |B'|.

Русский

Пусть B и B' — базы матроида M. Тогда |B| = |B'|.

LaTeX

$$$|B| = |B'|$$$

Lean4

theorem cardinalMk_eq (hB : M.IsBase B) (hB' : M.IsBase B') : #B = #B' :=
  hB.isBasis_ground.cardinalMk_eq hB'.isBasis_ground

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

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

Разделы

Аффилиация

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