perm_dlookup — Mathlib

English

If l1 is NodupKeys and l1 perm l2, then dlookup a l1 = dlookup a l2.

Русский

Если l1 имеет NodupKeys и l1 пермум с l2, то dlookup a l1 = dlookup a l2.

LaTeX

$$$ l_1.NodupKeys \\land l_1 \\sim l_2 \\implies dlookup\\ a\\ l_1 = dlookup\\ a\\ l_2 $$$

Lean4

theorem perm_dlookup (a : α) {l₁ l₂ : List (Sigma β)} (nd₁ : l₁.NodupKeys) (p : l₁ ~ l₂) :
    dlookup a l₁ = dlookup a l₂ := by
  have nd₂ := (perm_nodupKeys p).mp nd₁
  ext b; simp only [← Option.mem_def, mem_dlookup_iff nd₁, mem_dlookup_iff nd₂, p.mem_iff]

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