cardinalMk_le_cRank

Mathlib.Combinatorics.Matroid.Rank.Cardinal

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

English

If B is a base of M, then the size of B is at most the rank of M, i.e., #B ≤ cRank(M).

Русский

Если B — база M, то её размер не превышает ранг M: #B ≤ cRank(M).

LaTeX

$$$\\#B \\le M.\\mathrm{cRank}$$$

Lean4

theorem cardinalMk_le_cRank (hB : M.IsBase B) : #B ≤ M.cRank :=
  le_ciSup (f := fun B : { B // M.IsBase B } ↦ #B.1) (bddAbove_range _) ⟨B, hB⟩

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

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

Разделы

Аффилиация

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