English
Two finsupps are equal iff they have equal supports and agree on every element of the first support.
Русский
Две finsupp равны тогда и только тогда, когда их опоры равны и они совпадают на каждом элементе опоры.
LaTeX
$$$f = g \\iff f.\\\\operatorname{support} = g.\\\\operatorname{support} \\\\wedge \\\\forall x \\in f.\\\\operatorname{support}, f x = g x$$$
Lean4
theorem ext_iff' {f g : α →₀ M} : f = g ↔ f.support = g.support ∧ ∀ x ∈ f.support, f x = g x :=
⟨fun h => h ▸ ⟨rfl, fun _ _ => rfl⟩, fun ⟨h₁, h₂⟩ =>
ext fun a => by
classical
exact
if h : a ∈ f.support then h₂ a h
else by
have hf : f a = 0 := notMem_support_iff.1 h
have hg : g a = 0 := by rwa [h₁, notMem_support_iff] at h
rw [hf, hg]⟩
