isBase_of_le_cRank_of_finite — Mathlib

English

Let h : M.Spanning X, le : #X ≤ M.cRank, fin : X.Finite. Then X is a base: M.IsBase X.

Русский

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

LaTeX

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

Lean4

theorem isBase_of_le_cRank_of_finite (h : M.Spanning X) (le : #X ≤ M.cRank) (fin : X.Finite) : M.IsBase X :=
  have ⟨_B, hB, hBX⟩ := h.exists_isBase_subset
  have := hB.rankFinite_of_finite (fin.subset hBX)
  h.isBase_of_le_cRank le

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