eRank_le_encard_add_eRk_compl — Mathlib

English

The (global) eRank is bounded by encard of a set and the rank on its complement: eRank ≤ X.encard + eRk(E \\ X).

Русский

Глобальный eRank ограничен encard множества X и рангом дополнения E \\ X.

LaTeX

$$$M.eRank \\le X.encard + M.eRk(M.E \\ X)$$$

Lean4

theorem eRank_le_encard_add_eRk_compl (M : Matroid α) (X : Set α) : M.eRank ≤ X.encard + M.eRk (M.E \ X) :=
  le_trans (by rw [← eRk_inter_ground, eRank_def, union_diff_self, union_inter_cancel_right])
    (M.eRk_union_le_encard_add_eRk X (M.E \ X))

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