eRk_dual_add_eRank' — Mathlib

English

For any M and X, M✶.eRk X + M.eRank = M.eRk(M.E \\ X) + (X ∩ M.E).encard.

Русский

Для любого M и X: M✶.eRk X + M.eRank = M.eRk(M.E \\ X) + (X ∩ M.E).encard.

LaTeX

$$$ M^{\\ast}.\\mathrm{eRk}~X + M.\\mathrm{eRank} = M.\\mathrm{eRk}(M.E \\ X) + (X \\cap M.E).encard $$$

Lean4

/-- A version of `Matroid.dual_eRk_add_eRank` for non-subsets of the ground set. -/
theorem eRk_dual_add_eRank' (M : Matroid α) (X : Set α) : M✶.eRk X + M.eRank = M.eRk (M.E \ X) + (X ∩ M.E).encard := by
  rw [← diff_inter_self_eq_diff, ← eRk_dual_add_eRank .., ← dual_ground, eRk_inter_ground]

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