kinsert — Mathlib

English

If l1 and l2 are permutations of each other and l1 has NodupKeys, then kinsert a b l1 and kinsert a b l2 are also permutations.

Русский

Если l1 и l2 равны по перестановке и l1 имеет уникальные ключи, то kinsert a b l1 и kinsert a b l2 также взаимно переставимы.

LaTeX

$$$l_1 \\sim l_2 \\;\\Rightarrow\\; (kinsert a b l_1) \\sim (kinsert a b l_2)$$$

Lean4

theorem kinsert {a} {b : β a} {l₁ l₂ : List (Sigma β)} (nd₁ : l₁.NodupKeys) (p : l₁ ~ l₂) :
    kinsert a b l₁ ~ kinsert a b l₂ :=
  (p.kerase nd₁).cons _

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