isBase_of_cRank_le — Mathlib

English

Let M be a matroid with finite rank. If I is independent and the cardinal rank satisfies cRank(M) ≤ |I|, then I is a base of M.

Русский

Пусть M — матроид с конечным рангом. Если I независимо в M и cRank(M) ≤ |I|, то I является базой M.

LaTeX

$$$ M.Indep(I) \\wedge M.cRank \\le |I| \\;\Rightarrow\; M.IsBase(I) $$$

Lean4

theorem isBase_of_cRank_le [M.RankFinite] (ind : M.Indep I) (le : M.cRank ≤ #I) : M.IsBase I :=
  ind.isBase_of_maximal fun _J ind_J hIJ ↦
    ind.finite.eq_of_subset_of_encard_le hIJ <| toENat.monotone' <| ind_J.cardinalMk_le_cRank.trans le

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