eRk_union_le_encard_add_eRk

Mathlib.Combinatorics.Matroid.Rank.ENat

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

← MathLib Explorer

English

For X,Y ⊆ α, eRk(X ∪ Y) ≤ X.encard + eRk(Y).

Русский

Для X,Y ⊆ α имеет место неравенство eRk(X ∪ Y) ≤ X.encard + eRk(Y).

LaTeX

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

Lean4

theorem eRk_union_le_encard_add_eRk (M : Matroid α) (X Y : Set α) : M.eRk (X ∪ Y) ≤ X.encard + M.eRk Y :=
  (M.eRk_union_le_eRk_add_eRk X Y).trans <| add_le_add_right (M.eRk_le_encard _) _

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

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

Разделы

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

Аффилиация

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