support_nonempty_iff — Mathlib

English

Let f be a finitely supported function f: α → M. Then its support is nonempty iff f ≠ 0.

Русский

Пусть f — функция с конечной опорой f: α → M. Тогда опора f непуста тогда и только тогда, когда f ≠ 0.

LaTeX

$$$\\operatorname{supp}(f) \\neq \\emptyset \\iff f \\neq 0$$$

Lean4

theorem support_nonempty_iff {f : α →₀ M} : f.support.Nonempty ↔ f ≠ 0 := by
  simp only [Finsupp.support_eq_empty, Finset.nonempty_iff_ne_empty, Ne]

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