finrank_add_finrank_le_of_disjoint

English

The submodule generated by a finite set A is finite-dimensional.

Русский

Подпространство, порождаемое конечным множеством A, конечномерно.

LaTeX

$$FiniteDimensional K (span K A)$$

Lean4

theorem finrank_add_finrank_le_of_disjoint [FiniteDimensional K V] {s t : Submodule K V} (hdisjoint : Disjoint s t) :
    finrank K s + finrank K t ≤ finrank K V :=
  by
  rw [← Submodule.finrank_sup_add_finrank_inf_eq s t, hdisjoint.eq_bot, finrank_bot, add_zero]
  exact Submodule.finrank_le _

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