mem_ext — Mathlib

English

If two NodupKeys lists have the same membership predicate for every element, then they are Perm equivalent.

Русский

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

LaTeX

$$$ l_0.NodupKeys \\land l_1.NodupKeys \\land (\\forall x, x \\in l_0 \\leftrightarrow x \\in l_1) \\Rightarrow l_0 \\sim l_1 $$$

Lean4

theorem mem_ext {l₀ l₁ : List (Sigma β)} (nd₀ : l₀.Nodup) (nd₁ : l₁.Nodup) (h : ∀ x, x ∈ l₀ ↔ x ∈ l₁) : l₀ ~ l₁ := by
  grind [perm_ext_iff_of_nodup]

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