mem_supported' — Mathlib

English

Equivalently, p is in the supported submodule on s if and only if every x outside s has p(x) = 0.

Русский

Эквивалентно: p ∈ поддерживаемый на s тогда и только тогда, когда для любого x ∉ s выполняется p(x) = 0.

LaTeX

$$$p \in \mathrm{supported}(M,R,s) \iff \forall x, x \notin s \Rightarrow p(x) = 0$$$

Lean4

theorem mem_supported' {s : Set α} (p : α →₀ M) : p ∈ supported M R s ↔ ∀ x ∉ s, p x = 0 := by
  simp [mem_supported, Set.subset_def, not_imp_comm]

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