isBase_of_le_cRank — Mathlib

English

Let M be a matroid with finite rank. If X is spanning and the size of X is at most the rank, then X is a base.

Русский

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

LaTeX

$$$ M.Spanning(X) \\land |X| \\le M.cRank \\Rightarrow M.IsBase(X) $$$

Lean4

theorem isBase_of_le_cRank [M.RankFinite] (h : M.Spanning X) (le : #X ≤ M.cRank) : M.IsBase X :=
  by
  have ⟨B, hB, hBX⟩ := h.exists_isBase_subset
  rwa [← hB.finite.eq_of_subset_of_encard_le hBX (toENat.monotone' <| le.trans hB.cardinalMk_eq_cRank.ge)]

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