of_finite_basis — Mathlib

English

If a space has a basis indexed by a finite set, then the space is finite-dimensional.

Русский

Если пространство имеет базис, индексируемый конечным множеством, то пространство конечномерно.

LaTeX

$$$\exists ι\ (\text{Finite}(ι) \land \text{Basis } ι K V) \Rightarrow \operatorname{FiniteDimensional} K V$$$

Lean4

/-- If a vector space has a basis indexed by elements of a finite set, then it is
finite-dimensional. -/
theorem of_finite_basis {ι : Type w} {s : Set ι} (h : Basis s K V) (hs : Set.Finite s) : FiniteDimensional K V :=
  haveI := hs.fintype
  of_fintype_basis h

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