single_mem_supported — Mathlib

English

If a ∈ s, then the singleton function at a with value b lies in the supported submodule on s.

Русский

Если элемент a принадлежит s, то отображение, имеющее на позиции a значение b и ноль в прочих позициях, принадлежит поддерживаемому подмодулю на s.

LaTeX

$$If $a \in s$ then $\mathrm{single}(a,b) \in \mathrm{supported}(M,R,s)$.$$

Lean4

theorem single_mem_supported {s : Set α} {a : α} (b : M) (h : a ∈ s) : single a b ∈ supported M R s :=
  Set.Subset.trans support_single_subset (Finset.singleton_subset_set_iff.2 h)

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