eRk_le_eRk_add_eRk_diff

Mathlib.Combinatorics.Matroid.Rank.ENat

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

← MathLib Explorer

English

If Y ⊆ X then eRk(X) ≤ eRk(X ∩ Y) + eRk(X \\ Y).

Русский

Если Y ⊆ X, то eRk(X) ≤ eRk(X ∩ Y) + eRk(X \\ Y).

LaTeX

$$$M.eRk X \\le M.eRk(X \\cap Y) + M.eRk(X \\setminus Y)$$$

Lean4

theorem eRk_le_eRk_add_eRk_diff (M : Matroid α) (h : Y ⊆ X) : M.eRk X ≤ M.eRk Y + M.eRk (X \ Y) := by
  nth_rw 1 [← union_diff_cancel h]; apply eRk_union_le_eRk_add_eRk

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

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

Разделы

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

Аффилиация

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