perm_lookupAll — Mathlib

English

If l1 has NodupKeys and l1 is a permutation of l2, then lookupAll a l1 = lookupAll a l2.

Русский

Если l1 имеет NodupKeys и является перестановкой l2, то lookupAll a l1 = lookupAll a l2.

LaTeX

$$$ \mathrm{lookupAll} a\ l_1 = \mathrm{lookupAll} a\ l_2 $$$

Lean4

theorem perm_lookupAll (a : α) {l₁ l₂ : List (Sigma β)} (nd₁ : l₁.NodupKeys) (p : l₁ ~ l₂) :
    lookupAll a l₁ = lookupAll a l₂ := by
  have nd₂ := (perm_nodupKeys p).mp nd₁
  simp [lookupAll_eq_dlookup, nd₁, nd₂, perm_dlookup a nd₁ p]

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