keys_ext — Mathlib

English

Two Finmaps built from AList representations have equal keys iff the AList key lists are permutations of each other.

Русский

Два Finmap, построенные из представлений AList, имеют равные ключи тогда и только тогда, когда списки ключей AList взаимно переставлены.

LaTeX

$$$$ \forall {s_1 s_2 : AList \beta}, \mathrm{keys}(\langle s_1 \rangle) = \mathrm{keys}(\langle s_2 \rangle) \leftrightarrow s_1.\mathrm{keys} \sim s_2.\mathrm{keys} $$$$

Lean4

@[simp]
theorem keys_ext {s₁ s₂ : AList β} : keys ⟦s₁⟧ = keys ⟦s₂⟧ ↔ s₁.keys ~ s₂.keys := by simp [keys, AList.keys]

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