mk_eq_mk_of_basis'

Mathlib.LinearAlgebra.Dimension.StrongRankCondition

URI: https://scilib.ai/kg/mathlib#mk_eq_mk_of_basis'

English

The cardinalities of index sets of two bases are equal: |ι| = |ι'|.

Русский

Кардинальности множеств индексов двух баз равны: |ι| = |ι'|.

LaTeX

$$$|\iota| = |\iota'|$ for bases $v$ and $v'$.$$

Lean4

theorem mk_eq_mk_of_basis' {ι' : Type w} (v : Basis ι R M) (v' : Basis ι' R M) : #ι = #ι' :=
  Cardinal.lift_inj.1 <| mk_eq_mk_of_basis v v'

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru