cardinalMk_diff_comm

Mathlib.Combinatorics.Matroid.Rank.Cardinal

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

← MathLib Explorer

English

If I and J are bases of X in M, then # (I \\ J) = # (J \\ I).

Русский

Если I и J — базы X в M, то кардинал(I \\ J) = кардинал(J \\ I).

LaTeX

$$$\\#(I \\setminus J) = \\#(J \\setminus I)$$$

Lean4

theorem cardinalMk_diff_comm (hIX : M.IsBasis I X) (hJX : M.IsBasis J X) : #(I \ J : Set α) = #(J \ I : Set α) :=
  InvariantCardinalRank.forall_card_isBasis_diff hIX hJX

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

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

Разделы

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

Аффилиация

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