nodupKeys_middle — Mathlib

English

NodupKeys is preserved when moving a single element from the middle between two lists; the middle lemma equates NodupKeys for l1 ++ s :: l2 with s :: (l1 ++ l2).

Русский

Сохранение NodupKeys при помещении элемента s между двумя списками: NodupKeys (l1 ++ s :: l2) эквивалентно NodupKeys (s :: (l1 ++ l2)).

LaTeX

$$$ (l_1 ++ s :: l_2).NodupKeys \\iff (s :: (l_1 ++ l_2)).NodupKeys $$$

Lean4

theorem nodupKeys_middle {s : Sigma β} : (l₁ ++ s :: l₂).NodupKeys ↔ (s :: (l₁ ++ l₂)).NodupKeys := by
  simp_all [NodupKeys, keys, nodup_middle]

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