isCompl_span_singleton_of_isCoatom_of_notMem

English

If s is a maximal proper subspace of a vector space V over a division ring K and x ∉ s, then the subspaces s and the span of x form a direct complement: s ∩ (K·x) = {0} and s + (K·x) = V.

Русский

Если s является коатомом (максимальным собственным подпространством) пространства V над полем K и x ∉ s, то s и izdels’ спан x образуют прямое дополнение: s ∩ (K·x) = {0} и s + (K·x) = V.

LaTeX

$$$IsCompl\, s\ (K \cdot x)$$$

Lean4

theorem isCompl_span_singleton_of_isCoatom_of_notMem (hs : IsCoatom s) (hx : x ∉ s) : IsCompl s (K ∙ x) :=
  by
  refine ⟨disjoint_span_singleton_of_notMem hx, ?_⟩
  rw [← covBy_top_iff] at hs
  simpa only [codisjoint_iff, sup_comm, not_lt_top_iff] using hs.2 (covBy_span_singleton_sup hx).1

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