lookup_ext — Mathlib

English

Under a permutation, dlookup is preserved; a simple consequence of perm_dlookup.

Русский

При перестановке сохраняется dlookup; простое следствие perm_dlookup.

LaTeX

$$$ (l_1 \\sim l_2) \\implies \\mathrm{dlookup}\\ a\\ l_1 = \\mathrm{dlookup}\\ a\\ l_2 $$$

Lean4

theorem lookup_ext {l₀ l₁ : List (Sigma β)} (nd₀ : l₀.NodupKeys) (nd₁ : l₁.NodupKeys)
    (h : ∀ x y, y ∈ l₀.dlookup x ↔ y ∈ l₁.dlookup x) : l₀ ~ l₁ := by grind [_=_ mem_dlookup_iff, mem_ext]

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