supported_eq_span_single — Mathlib

English

The supported submodule on s equals the linear span of the delta functions on s.

Русский

Подмодуль, поддерживаемый на s, равен линейному замыканию дельта-функций на s.

LaTeX

$$$\mathrm{supported}(M,R,s) = \operatorname{span}_R\{\mathrm{single}(i,1) : i \in s\}$$$

Lean4

theorem supported_eq_span_single (s : Set α) : supported R R s = span R ((fun i => single i 1) '' s) :=
  by
  refine (span_eq_of_le _ ?_ (SetLike.le_def.2 fun l hl => ?_)).symm
  · rintro _ ⟨_, hp, rfl⟩
    exact single_mem_supported R 1 hp
  · rw [← l.sum_single]
    refine sum_mem fun i il => ?_
    rw [show single i (l i) = l i • single i 1 by simp]
    exact smul_mem _ (l i) (subset_span (mem_image_of_mem _ (hl il)))

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