English
If two Finmaps β have identical lookup results at every key, then the Finmaps are equal.
Русский
Если две отображения Finmap β совпадают по значениям поиска для каждого ключа, то эти отображения равны.
LaTeX
$$$ \forall s_1 \ s_2 : Finmap\, \beta, \ (\forall x: \alpha, \operatorname{lookup}(x,s_1) = \operatorname{lookup}(x,s_2)) \Rightarrow s_1 = s_2. $$$
Lean4
theorem ext_lookup {s₁ s₂ : Finmap β} : (∀ x, s₁.lookup x = s₂.lookup x) → s₁ = s₂ :=
induction_on₂ s₁ s₂ fun s₁ s₂ h => by
simp only [AList.lookup, lookup_toFinmap] at h
rw [AList.toFinmap_eq]
apply lookup_ext s₁.nodupKeys s₂.nodupKeys
intro x y
rw [h]
