notMem_span_image — Mathlib

English

If hv is LinearIndependent on v, then for any x ∉ s, v x ∉ span R (v '' s).

Русский

Если v линейно независимо на s, то для любого x не принадлежащего s, v x не принадлежит линейной оболочке v '' s.

LaTeX

$$v x ∉ span_R (v '' s)$$

Lean4

theorem notMem_span_image [Nontrivial R] (hv : LinearIndependent R v) {s : Set ι} {x : ι} (h : x ∉ s) :
    v x ∉ Submodule.span R (v '' s) :=
  by
  have h' : v x ∈ Submodule.span R (v '' { x }) :=
    by
    rw [Set.image_singleton]
    exact mem_span_singleton_self (v x)
  intro w
  apply LinearIndependent.ne_zero x hv
  refine disjoint_def.1 (hv.disjoint_span_image ?_) (v x) h' w
  simpa using h

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