encard_eq_encard — Mathlib

English

Let M be a matroid and X a subset of its ground set. If I and J are bases of X (i.e., both are bases in the restriction M|X), then encard(I) = encard(J); in particular, all bases of X have the same encard.

Русский

Пусть M — матроид на некотором множестве, и X ⊆ E. Если I и J являются базами множества X (то есть базами ограниченного матоида M|X), то encard(I) = encard(J); следовательно, все базы X имеют одинаковую encard.

LaTeX

$$$\\operatorname{encard}(I) = \\operatorname{encard}(J)$$$

Lean4

theorem encard_eq_encard (hI : M.IsBasis I X) (hJ : M.IsBasis J X) : I.encard = J.encard :=
  hI.isBasis'.encard_eq_encard hJ.isBasis'

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