self_mem_span_image — Mathlib

English

The range of the linear map b.repr equals the full finitely-supported functions ι → R, i.e. the coordinate representation covers all finitely supported vectors.

Русский

Область отображения b.repr совпадает с полем всех конечносопряженных функций ι → R.

LaTeX

$$$\operatorname{range}(b^{\wedge}) = \mathsf{Finsupp}(\,ι, R\,).$$$

Lean4

@[simp]
theorem self_mem_span_image [Nontrivial R] {i : ι} {s : Set ι} : b i ∈ span R (b '' s) ↔ i ∈ s := by
  simp [mem_span_image, Finsupp.support_single_ne_zero]

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