range_linearCombination — Mathlib

English

The same as 129108: if v is surjective, range(linearCombination_R v) = ⊤.

Русский

То же самое, что и ранее: если $v$ сюръективно порождает пространство, образ линейной комбинации равен верхнему подмодулю.

LaTeX

$$$\operatorname{range}(\operatorname{linearCombination}_R(v)) = \top$$$

Lean4

theorem range_linearCombination : LinearMap.range (linearCombination R v) = span R (range v) :=
  by
  ext x
  constructor
  · intro hx
    rw [LinearMap.mem_range] at hx
    rcases hx with ⟨l, hl⟩
    rw [← hl]
    rw [linearCombination_apply]
    exact sum_mem fun i _ => Submodule.smul_mem _ _ (subset_span (mem_range_self i))
  · apply span_le.2
    intro x hx
    rcases hx with ⟨i, hi⟩
    rw [SetLike.mem_coe, LinearMap.mem_range]
    use single i 1
    simp [hi]

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