wellOrderedBasis — Mathlib

English

There exists a basis of E over F indexed by the initial ordinal, i.e. a basis whose indexing set is the ordinal type of the dimension (Module.rank F E).

Русский

Существует база пространства E над полем F, индексированная начальным порядком (база, индексируемая ординальным типом размерности).

LaTeX

$$$$\\text{wellOrderedBasis } : \\text{Basis } \\big( (\\mathrm{Module.rank } F E).ord.toType \\big) F E$$$$

Lean4

/-- A basis of E/F indexed by the initial ordinal. -/
def wellOrderedBasis : Basis ι F E :=
  (chooseBasis F E).reindex (Cardinal.eq.mp <| (mk_ord_toType _).trans <| rank_eq_card_chooseBasisIndex F E).some.symm

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