perm_nodupKeys

Mathlib.Data.List.Sigma

URI: https://scilib.ai/kg/mathlib#List.perm_nodupKeys

English

NodupKeys is preserved under list permutation: l1 ~ l2 implies NodupKeys l1 iff NodupKeys l2.

Русский

Условие перестановки списка сохраняет NodupKeys: l1 ~ l2 → NodupKeys l1 ⇔ NodupKeys l2.

LaTeX

$$$ l_1 \\sim l_2 \\implies (\\mathrm{NodupKeys}(l_1) \\iff \\mathrm{NodupKeys}(l_2)) $$$

Lean4

theorem perm_nodupKeys {l₁ l₂ : List (Sigma β)} (h : l₁ ~ l₂) : NodupKeys l₁ ↔ NodupKeys l₂ :=
  (h.map _).nodup_iff

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru