range_diagonal — Mathlib

English

The range of the linear map toLin'(diagonal w) is the supremum over indices i with w_i ≠ 0 of the ranges of the single-entry maps.

Русский

Образ отображения toLin'(diag(w)) равен объедению(супремуму) образов отображения single на индексы i с w_i ≠ 0.

LaTeX

$$range (toLin'(diagonal w)) = ⨆ i ∈ {i | w i ≠ 0}, range (single i)$$

Lean4

theorem range_diagonal [DecidableEq m] (w : m → K) :
    LinearMap.range (toLin' (diagonal w)) = ⨆ i ∈ {i | w i ≠ 0}, LinearMap.range (LinearMap.single K (fun _ => K) i) :=
  by
  dsimp only [mem_setOf_eq]
  rw [← Submodule.map_top, ← iSup_range_single, Submodule.map_iSup]
  congr; funext i
  rw [← LinearMap.range_comp, diagonal_comp_single, ← range_smul']

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