cardinal_lt_aleph0_of_finiteDimensional

English

If K is finite, and V is a finite-dimensional free K-vector space, then V has finite cardinality.

Русский

Если K конечно, и V — свободное конечномерное пространство над K, то множество V конечно.

LaTeX

$$[Finite K] [Module.Free K V] [Module.Finite K V] ⇒ |V| < aleph0$$

Lean4

theorem cardinal_lt_aleph0_of_finiteDimensional [Finite K] [Module.Free K V] [Module.Finite K V] : #V < ℵ₀ :=
  by
  rw [← lift_lt_aleph0.{v, u}, lift_cardinalMk_eq_lift_cardinalMk_field_pow_lift_rank K V]
  exact power_lt_aleph0 (lift_lt_aleph0.2 (lt_aleph0_of_finite K)) (lift_lt_aleph0.2 (rank_lt_aleph0 K V))

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