cardinalMk_diff_comm

Mathlib.Combinatorics.Matroid.Rank.Cardinal

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

← MathLib Explorer

English

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

Русский

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

LaTeX

$$$|B \setminus B'| = |B' \setminus B|$$$

Lean4

theorem cardinalMk_diff_comm (hB : M.IsBase B) (hB' : M.IsBase B') : #(B \ B' : Set α) = #(B' \ B : Set α) :=
  hB.isBasis_ground.cardinalMk_diff_comm hB'.isBasis_ground

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

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

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

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