cRk_le_of_subset

Mathlib.Combinatorics.Matroid.Rank.Cardinal

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

English

The function M.cRk is monotone with respect to subset inclusion: X ⊆ Y implies cRk X ≤ cRk Y.

Русский

Функция cRk монотонна по включению: X ⊆ Y ⇒ cRk(X) ≤ cRk(Y).

LaTeX

$$$X \\subseteq Y \\Rightarrow M.\\mathrm{cRk} X \\le M.\\mathrm{cRk} Y$$$

Lean4

theorem cRk_le_of_subset (M : Matroid α) (hXY : X ⊆ Y) : M.cRk X ≤ M.cRk Y :=
  M.cRk_mono hXY

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

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

Разделы

Аффилиация

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