span_image_extend_eq_span_image — Mathlib

English

The span of the images under v of the extended set equals the span of the images of t.

Русский

Порождающее множество образов v по расширенному набору эквивалентно порождающему множество образов v по t.

LaTeX

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

Lean4

theorem span_image_extend_eq_span_image (hs : LinearIndepOn K v s) (hst : s ⊆ t) :
    span K (v '' hs.extend hst) = span K (v '' t) :=
  le_antisymm (span_mono (image_mono (hs.extend_subset hst))) (span_le.2 (hs.image_subset_span_image_extend hst))

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