finite_index_of_rank_lt_aleph0 — Mathlib

English

If a basis b of a submodule s has rank less than aleph0, then s is finite.

Русский

Если база b подмодуля s имеет ранг < ℵ0, то s конечно.

LaTeX

$$$\text{Rank}_R s < \aleph0 \Rightarrow s \text{ is finite}.$$$

Lean4

/-- If a module has a finite dimension, all bases are indexed by a finite set. -/
theorem finite_index_of_rank_lt_aleph0 {ι : Type*} {s : Set ι} (b : Basis s R M) (h : Module.rank R M < ℵ₀) :
    s.Finite :=
  Set.finite_def.2 (b.nonempty_fintype_index_of_rank_lt_aleph0 h)

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