mem_supported — Mathlib

English

A finitely supported map p belongs to the supported submodule on s exactly when its support is contained in s.

Русский

Отображение p принадлежит поддерживаемому подмодулю на s тогда и только тогда, когда опора p ⊆ s.

LaTeX

$$$p \in \mathrm{supported}(M,R,s) \iff p\text{-support} ⊆ s$$$

Lean4

theorem mem_supported {s : Set α} (p : α →₀ M) : p ∈ supported M R s ↔ ↑p.support ⊆ s :=
  Iff.rfl

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