eq_of_mem_iff — Mathlib

English

If two sorted lists are the same with respect to membership of each element, then the lists are equal.

Русский

Если два отсортированных списка имеют одинаковые множества элементов, следовательно списки равны.

LaTeX

$$$(\\forall a, a \\in l_1 \\Leftrightarrow a \\in l_2) \\to l_1 = l_2$ (при условиях антисимметрии и неизменности) $$

Lean4

theorem eq_of_mem_iff [IsAntisymm α r] [IsIrrefl α r] {l₁ l₂ : List α} (h₁ : Sorted r l₁) (h₂ : Sorted r l₂)
    (h : ∀ a : α, a ∈ l₁ ↔ a ∈ l₂) : l₁ = l₂ :=
  eq_of_perm_of_sorted ((perm_ext_iff_of_nodup h₁.nodup h₂.nodup).2 h) h₁ h₂

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