support_subset_iff — Mathlib

English

The support of f is contained in s iff for every a not in s, f(a) = 0.

Русский

Опора f содержится в s тогда и только тогда, когда для каждого a вне s выполняется f(a) = 0.

LaTeX

$$\operatorname{supp}(f) \\subseteq s \\iff \\forall a \\notin s,\\ f(a) = 0$$

Lean4

theorem support_subset_iff {s : Set α} {f : α →₀ M} : ↑f.support ⊆ s ↔ ∀ a ∉ s, f a = 0 := by
  simp only [Set.subset_def, mem_coe, mem_support_iff, forall_congr' fun a => not_imp_comm]

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