nodupKeys_iff_pairwise

Mathlib.Data.List.Sigma

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

English

The property NodupKeys l is equivalent to Pairwise (fun s s' => s.1 ≠ s'.1) l.

Русский

Свойство NodupKeys l эквивалентно Pairwise (fun s s' => s.1 ≠ s'.1) l.

LaTeX

$$$ NodupKeys\ l \\iff Pairwise\\big(\\lambda s s' : \\Sigma \\beta,\\ s.1 \\neq s'.1\\big)\\ l. $$$

Lean4

theorem nodupKeys_iff_pairwise {l} : NodupKeys l ↔ Pairwise (fun s s' : Sigma β => s.1 ≠ s'.1) l :=
  pairwise_map

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

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

Разделы

Аффилиация

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