cRank_le_cardinalMk

Mathlib.Combinatorics.Matroid.Rank.Cardinal

URI: https://scilib.ai/kg/mathlib#Matroid.Spanning.cRank_le_cardinalMk

← MathLib Explorer

English

If X is spanning, then cRank ≤ |X|.

Русский

Если X является покрывающей, то cRank ≤ |X|.

LaTeX

$$$cRank \le |X|$ (when $M$ is spanning $X$)$$

Lean4

theorem cRank_le_cardinalMk (h : M.Spanning X) : M.cRank ≤ #X :=
  have ⟨_B, hB, hBX⟩ := h.exists_isBase_subset
  (hB.cardinalMk_eq_cRank).symm.trans_le (mk_le_mk_of_subset hBX)

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

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

Разделы

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

Аффилиация

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