covBy_span_singleton_sup — Mathlib

English

There is no CovBy between s and (span {x}) ⊔ s when x ∉ s.

Русский

Если x не в s, то CovBy между s и (span {x}) ⊔ s отсутствует.

LaTeX

$$$CovBy\, s\, (\operatorname{span}\;\{x\} \;⊔\; s)$$$

Lean4

/-- There is no vector subspace between `s` and `(K ∙ x) ⊔ s`, `CovBy` version. -/
theorem covBy_span_singleton_sup {x : V} {s : Submodule K V} (h : x ∉ s) : CovBy s ((K ∙ x) ⊔ s) :=
  ⟨by simpa, (wcovBy_span_singleton_sup _ _).2⟩

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