eq_top_of_disjoint — Mathlib

English

The submodule generated by a single element is finite-dimensional.

Русский

Подпространство, порождаемое одним элементом, конечномерно.

LaTeX

$$FiniteDimensional K (K ∙ x)$$

Lean4

theorem eq_top_of_disjoint [FiniteDimensional K V] (s t : Submodule K V)
    (hdim : finrank K V ≤ finrank K s + finrank K t) (hdisjoint : Disjoint s t) : s ⊔ t = ⊤ :=
  by
  have h_finrank_inf : finrank K ↑(s ⊓ t) = 0 :=
    by
    rw [disjoint_iff_inf_le, le_bot_iff] at hdisjoint
    rw [hdisjoint, finrank_bot]
  apply eq_top_of_finrank_eq
  replace hdim : finrank K V = finrank K s + finrank K t :=
    le_antisymm hdim (finrank_add_finrank_le_of_disjoint hdisjoint)
  rw [hdim]
  convert s.finrank_sup_add_finrank_inf_eq t
  rw [h_finrank_inf]
  rfl

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