mem_supported_support — Mathlib

English

For any p, the function lies in the supported submodule on its own support.

Русский

Для любого p функция принадлежит поддерживаемому подмодулю на своей собственной опоре.

LaTeX

$$For any $p$, one has $p \in \mathrm{supported}(M,R, p.{\text{support}})$.$$

Lean4

theorem mem_supported_support (p : α →₀ M) : p ∈ Finsupp.supported M R (p.support : Set α) := by
  rw [Finsupp.mem_supported]

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