span_extend_eq_span — Mathlib

English

The span of the extended set equals the span of t.

Русский

Порождающее множество расширенного набора равняется порождающему множество t.

LaTeX

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

Lean4

theorem span_extend_eq_span {s t : Set V} (hs : LinearIndepOn K id s) (hst : s ⊆ t) :
    span K (hs.extend hst) = span K t :=
  le_antisymm (span_mono (hs.extend_subset hst)) (span_le.2 (hs.subset_span_extend hst))

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