lt_aleph0_of_finiteDimensional — Mathlib

English

In a finite-dimensional vector space over a division ring, any linearly independent family has index set of cardinality less than aleph_0.

Русский

В конечномерном векторном пространстве над кольцом делений любая линейно независимая система имеет индексное множество меньшей мощности, чем aleph_0.

LaTeX

$$$ \#\iota < \aleph_0 \quad \text{if } [FiniteDimensional K V] \ and\ h : LinearIndependent K v, \vphantom{a} $$$

Lean4

theorem _root_.LinearIndependent.lt_aleph0_of_finiteDimensional {ι : Type w} [FiniteDimensional K V] {v : ι → V}
    (h : LinearIndependent K v) : #ι < ℵ₀ :=
  h.lt_aleph0_of_finite

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