finite_basis_index — Mathlib

English

As above, the range of eval_i is the top subspace for finite σ.

Русский

Как выше, образ eval_i равен топ-подпространству при конечном σ.

LaTeX

$$$$ \\mathrm{range}(\\\\mathrm{eval}_{i}) = \\top. $$$$

Lean4

/-- In a Noetherian module over a division ring,
if a basis is indexed by a set, that set is finite. -/
theorem finite_basis_index {ι : Type*} {s : Set ι} [IsNoetherian K V] (b : Basis s K V) : s.Finite :=
  b.finite_index_of_rank_lt_aleph0 (rank_lt_aleph0 K V)

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