toFinmap_eq — Mathlib

English

Two AList representations yield the same Finmap iff their entry multisets are permutations of each other.

Русский

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

LaTeX

$$$$ toFinmap(s_1) = toFinmap(s_2) \iff s_1.entries \sim s_2.entries $$$$

Lean4

theorem toFinmap_eq {s₁ s₂ : AList β} : toFinmap s₁ = toFinmap s₂ ↔ s₁.entries ~ s₂.entries :=
  by
  cases s₁
  cases s₂
  simp [AList.toFinmap]

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