nonempty_fintype_index_of_rank_lt_aleph0

English

If a module has finite rank, then any basis indexed by ι with rank less than aleph0 has a nonempty fintype index.

Русский

Если ранг модуля конечен, то любой базис с индексацией ι и ранга < ℵ0 имеет непустой конечный индекс.

LaTeX

$$$[\text{Module.Rank } R M] < \aleph_0 \Rightarrow \text{Nonempty } (\text{Fintype } ι).$$$

Lean4

/-- If a module has a finite dimension, all bases are indexed by a finite type. -/
theorem nonempty_fintype_index_of_rank_lt_aleph0 {ι : Type*} (b : Basis ι R M) (h : Module.rank R M < ℵ₀) :
    Nonempty (Fintype ι) := by
  rwa [← Cardinal.lift_lt, ← b.mk_eq_rank, Cardinal.lift_aleph0, Cardinal.lift_lt_aleph0,
    Cardinal.lt_aleph0_iff_fintype] at h

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