ext_iff — Mathlib

English

The equivalence between toFinset equality and dedup permutation holds (simp variant).

Русский

Эквивалентность между равенством toFinset и перестановкой dedup сохраняется (симп-вариант).

LaTeX

$$$\\forall {l l' : \\mathsf{List}\\,\\alpha},\\; l.toFinset = l'.toFinset \\\\iff l.dedup.Perm l'.dedup$$$

Lean4

theorem ext_iff {a b : List α} : a.toFinset = b.toFinset ↔ ∀ x, x ∈ a ↔ x ∈ b := by
  simp only [Finset.ext_iff, mem_toFinset]

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