isBase_of_eRk_ge — Mathlib

English

If I is independent, finite, and eRk X ≥ eRk I with X ⊇ I, then I is a Basis for X.

Русский

Если I независимо и конечно, и eRk X ≥ eRk I при X ⊇ I, то I является базой для X.

LaTeX

$$If $I$ is independent, finite, and $M.eRk X \\ge M.eRk I$ with $I \\subseteq X$, then $M.IsBasis' I X$.$$

Lean4

theorem isBase_of_eRk_ge (hI : M.Indep I) (hIfin : I.Finite) (h : M.eRank ≤ M.eRk I) : M.IsBase I := by
  simpa using hI.isBasis_of_eRk_ge hIfin hI.subset_ground (M.eRk_ground.trans_le h)

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