support_subset_iff — Mathlib

English

For a set s, the support of f is contained in s exactly when f(i) = 0 for all i not in s.

Русский

Для множества s опора f содержится в s тогда и только тогда, когда f(i) = 0 для всех i не в s.

LaTeX

$$$\\uparrow f.{\\mathrm{support}} \\subseteq s \\;\\iff\\; \\forall i, i \\notin s \\Rightarrow f_i = 0$$$

Lean4

theorem support_subset_iff {s : Set ι} {f : Π₀ i, β i} : ↑f.support ⊆ s ↔ ∀ i ∉ s, f i = 0 := by
  simpa [Set.subset_def] using forall_congr' fun i => not_imp_comm

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