isBase_of_cRank_le_of_finite — Mathlib

English

Let ind : M.Indep I, le : M.cRank ≤ #I, fin : I.Finite. Then I is a base: M.IsBase I.

Русский

Пусть I независимо в M, и |I| ≥ cRank(M), и I конечно. Тогда I является базой: M.IsBase I.

LaTeX

$$(ind : M.Indep I) ∧ (le : M.cRank ≤ #I) ∧ (fin : I.Finite) → M.IsBase I$$

Lean4

theorem isBase_of_cRank_le_of_finite (ind : M.Indep I) (le : M.cRank ≤ #I) (fin : I.Finite) : M.IsBase I :=
  have := rankFinite_iff_cRank_lt_aleph0.mpr (le.trans_lt <| lt_aleph0_iff_finite.mpr fin)
  ind.isBase_of_cRank_le le

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