infinite_basis_le_maximal_linearIndependent

English

Over a ring, if b is an infinite basis and v is LI with maximality, then |ι| ≤ |κ|.

Русский

Для бесконечного базиса и максимальной LI-коллекции выполняется неравенство кардиналов.

LaTeX

$$$|\\iota| \\le |\\kappa|$$$

Lean4

/-- Over any ring `R`, if `b` is an infinite basis for a module `M`,
and `s` is a maximal linearly independent set,
then the cardinality of `b` is bounded by the cardinality of `s`.
-/
theorem infinite_basis_le_maximal_linearIndependent {ι : Type w} (b : Basis ι R M) [Infinite ι] {κ : Type w} (v : κ → M)
    (i : LinearIndependent R v) (m : i.Maximal) : #ι ≤ #κ :=
  Cardinal.lift_le.mp (infinite_basis_le_maximal_linearIndependent' b v i m)

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