cardinalMk_eq

Mathlib.Combinatorics.Matroid.Rank.Cardinal

URI: https://scilib.ai/kg/mathlib#Matroid.IsBasis'.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 (hIX : M.IsBasis' I X) (hJX : M.IsBasis' J X) : #I = #J :=
  hIX.isBasis_inter_ground.cardinalMk_eq hJX.isBasis_inter_ground

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

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

Разделы

Аффилиация

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