image_subset_span_image_extend — Mathlib

English

The image of t under v is contained in the span of the image of b, where b is the extended set.

Русский

Образ t под действием v содержится в span образа b, где b — расширенное множество.

LaTeX

$$$$v''t \subseteq \operatorname{span}_K(v''(hs.extend hst)).$$$$

Lean4

theorem image_subset_span_image_extend (hs : LinearIndepOn K v s) (hst : s ⊆ t) :
    v '' t ⊆ span K (v '' hs.extend hst) :=
  let ⟨_hbt, _hsb, htb, _hli⟩ := Classical.choose_spec (exists_linearIndepOn_extension hs hst)
  htb

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