kerase — Mathlib

English

If a list l has no duplicate keys, then kerase a l also has no duplicate keys. In particular, kerase preserves the nodup-key property.

Русский

Если у списка l нет повторяющихся ключей, то и kerase a l не имеет повторяющихся ключей. kerase сохраняет свойство без повторов ключей.

LaTeX

$$∀ {a} (nd : l.NodupKeys), (kerase a l).NodupKeys$$

Lean4

theorem kerase (a : α) : NodupKeys l → (kerase a l).NodupKeys :=
  NodupKeys.sublist <| kerase_sublist _ _

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