cRank_restrict

Mathlib.Combinatorics.Matroid.Rank.Cardinal

URI: https://scilib.ai/kg/mathlib#Matroid.cRank_restrict

English

The rank of the full ground equals the cRank of the matroid: cRk M.E = cRank(M).

Русский

Ранг множества всего основания равен cRank матроида: cRk(M.E) = cRank(M).

LaTeX

$$$M.\\mathrm{cRk} M.\\mathrm{E} = M.\\mathrm{cRank}$$$

Lean4

@[simp]
theorem cRank_restrict (M : Matroid α) (X : Set α) : (M ↾ X).cRank = M.cRk X :=
  rfl

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

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

Разделы

Аффилиация

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