mem_support_onFinset — Mathlib

English

An element a belongs to the support of onFinset if and only if f(a) ≠ 0.

Русский

Элемент a принадлежит опоре onFinset тогда и только тогда, когда f(a) ≠ 0.

LaTeX

$$a \in (onFinset s f hf).support \\iff f(a) \\neq 0$$

Lean4

theorem mem_support_onFinset {s : Finset α} {f : α → M} (hf : ∀ a : α, f a ≠ 0 → a ∈ s) {a : α} :
    a ∈ (Finsupp.onFinset s f hf).support ↔ f a ≠ 0 := by rw [Finsupp.mem_support_iff, Finsupp.onFinset_apply]

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