eRk_union_le_eRk_add_encard

Mathlib.Combinatorics.Matroid.Rank.ENat

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

← MathLib Explorer

English

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

Русский

Для X,Y ⊆ α, eRk(X ∪ Y) ≤ eRk(X) + Y.encard.

LaTeX

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

Lean4

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

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

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

Разделы

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

Аффилиация

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