lt_aleph0_of_finite — Mathlib

English

If M is finite over R, any linear independent family v: ι → M has cardinality strictly less than aleph0; i.e., #ι < ℵ0.

Русский

Если M конечно над R, любая линейно независимаяFamily v: ι → M имеет кардинал < ℵ0.

LaTeX

$$$[Module.Finite R M] \Rightarrow (\text{LinearIndependent } R v) \Rightarrow \#ι < \aleph0$$$

Lean4

theorem lt_aleph0_of_finite {ι : Type w} [Module.Finite R M] {v : ι → M} (h : LinearIndependent R v) : #ι < ℵ₀ :=
  by
  apply Cardinal.lift_lt.1
  apply lt_of_le_of_lt
  · apply h.cardinal_lift_le_rank
  · rw [← finrank_eq_rank, Cardinal.lift_aleph0, Cardinal.lift_natCast]
    apply Cardinal.nat_lt_aleph0

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