eRank_add_eRank_dual — Mathlib

English

For any matroid M, the sum of the eRank of M and the dual eRank of M equals the encard of the ground: eRank(M) + M✶.eRank = M.E.encard.

Русский

Для любого матроидa сумма eRank(M) и eRank двойственного матроида равна encard множества оснований M.E: eRank(M) + M✶.eRank = M.E.encard.

LaTeX

$$$ M.\\mathrm{eRank} + M^{\\ast}.\\mathrm{eRank} = M.E.encard $$$

Lean4

@[simp]
theorem eRank_add_eRank_dual (M : Matroid α) : M.eRank + M✶.eRank = M.E.encard :=
  by
  obtain ⟨B, hB⟩ := M.exists_isBase
  rw [← hB.encard_eq_eRank, ← hB.compl_isBase_dual.encard_eq_eRank, ← encard_union_eq disjoint_sdiff_right,
    union_diff_cancel hB.subset_ground]

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