linearCombinationOn_range — Mathlib

English

The range of linearCombinationOn is the whole target span, i.e., the map is surjective onto span R (v'' s).

Русский

Образ linearCombinationOn равен всему порождающему пространству, то есть отображение сюръективно на span R (v'' s).

LaTeX

$$$\\operatorname{range}(\\mathrm{linearCombinationOn}_{\\alpha,M,R}(v,s)) = \\top$$$

Lean4

theorem linearCombinationOn_range (s : Set α) : LinearMap.range (linearCombinationOn α M R v s) = ⊤ :=
  by
  rw [linearCombinationOn, LinearMap.range_eq_map, LinearMap.map_codRestrict, ← LinearMap.range_le_iff_comap,
    range_subtype, Submodule.map_top, LinearMap.range_comp, range_subtype]
  exact (span_image_eq_map_linearCombination _ _).le

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