card_le_card_of_linearIndependent

English

Let b be a basis of finite type; if v is linearly independent, then the cardinality of the index set of v is at most that of the basis, i.e., |ι'| ≤ |ι|.

Русский

Пусть базис b имеет конечное множество индексов; если v линейно независим, то |ι'| ≤ |ι|.

LaTeX

$$|\\iota'| \\le |\\iota|$$

Lean4

theorem card_le_card_of_linearIndependent {ι : Type*} [Fintype ι] (b : Basis ι R M) {ι' : Type*} [Fintype ι']
    {v : ι' → M} (hv : LinearIndependent R v) : Fintype.card ι' ≤ Fintype.card ι :=
  by
  letI := nontrivial_of_invariantBasisNumber R
  simpa [rank_eq_card_basis b, Cardinal.mk_fintype] using hv.cardinal_lift_le_rank

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