eRank_le_card_width — Mathlib

English

Under StrongRankCondition and finite n, eRank ≤ ENat.card n.

Русский

При условии StrongRankCondition и конечного n, eRank ≤ ENat.card n.

LaTeX

$$$A.eRank \le ENat.card\,n.$$$

Lean4

theorem eRank_le_card_width [StrongRankCondition R] (A : Matrix m n R) : A.eRank ≤ ENat.card n :=
  by
  wlog hfin : Finite n
  · simp [ENat.card_eq_top.2 (by simpa using hfin)]
  have _ := Fintype.ofFinite n
  rw [ENat.card_eq_coe_fintype_card, eRank, toENat_le_nat]
  exact A.cRank_le_card_width

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