aleph0_le_rank — Mathlib

English

If there is an infinite linearly independent family, then ℵ0 is less than or equal to the rank of M.

Русский

Если существует бесконечное линейно независимое множество, то ℵ0 не превосходит ранг M.

LaTeX

$$$\aleph_0 \le \operatorname{rank}_R(M)$$$

Lean4

theorem aleph0_le_rank {ι : Type w} [Infinite ι] {v : ι → M} (hv : LinearIndependent R v) : ℵ₀ ≤ Module.rank R M :=
  aleph0_le_lift.mp <| (aleph0_le_lift.mpr <| aleph0_le_mk ι).trans hv.cardinal_lift_le_rank

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