eRk_union_le_eRk_add_eRk

Mathlib.Combinatorics.Matroid.Rank.ENat

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

English

For any X,Y ⊆ α, the ENat-valued rank satisfies eRk(X ∪ Y) ≤ eRk(X) + eRk(Y).

Русский

Для любых X,Y выполняется неравенство субмодулярности по объединению: eRk(X ∪ Y) ≤ eRk(X) + eRk(Y).

LaTeX

$$$M.eRk(X \\cup Y) \\le M.eRk(X) + M.eRk(Y)$$$

Lean4

theorem eRk_union_le_eRk_add_eRk (M : Matroid α) (X Y : Set α) : M.eRk (X ∪ Y) ≤ M.eRk X + M.eRk Y :=
  le_add_self.trans (M.eRk_submod X Y)

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

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

Разделы

Аффилиация

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