encard_le_toENat_rank — Mathlib

English

For a linearly independent family, its encard is bounded by the ENat of the rank.

Русский

Для линейно независимого множества его encard не превышает ENat ранга.

LaTeX

$$$s.encard \le (\operatorname{rank}_R(M)).toENat$$$

Lean4

theorem _root_.LinearIndepOn.encard_le_toENat_rank {ι : Type*} {v : ι → M} {s : Set ι} (hs : LinearIndepOn R v s) :
    s.encard ≤ (Module.rank R M).toENat := by
  simpa using OrderHom.mono (β := ℕ∞) Cardinal.toENat hs.linearIndependent.cardinal_lift_le_rank

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