English
A finitely supported function f equals single a b if and only if its support is contained in {a} and f(a) = b.
Русский
Пусть f — конечноподдерживаемая функция. Тогда f = single a b тогда и только тогда, когда опора f ⊆ {a} и f(a) = b.
LaTeX
$$$$f = \\text{single } a\\, b \\iff \\operatorname{supp}(f) \\subseteq \\{a\\} \\land f(a)=b.$$$$
Lean4
theorem eq_single_iff {f : α →₀ M} {a b} : f = single a b ↔ f.support ⊆ { a } ∧ f a = b :=
by
refine ⟨fun h => h.symm ▸ ⟨support_single_subset, single_eq_same⟩, ?_⟩
rintro ⟨h, rfl⟩
ext x
by_cases hx : x = a <;> simp only [hx, single_eq_same, single_eq_of_ne, Ne, not_false_iff]
exact notMem_support_iff.1 (mt (fun hx => (mem_singleton.1 (h hx))) hx)
