of_map

Mathlib.Data.List.Nodup

URI: https://scilib.ai/kg/mathlib#List.Nodup.of_map

English

If map f l is nodup, then l is nodup.

Русский

Если отображение f на l дают безповторный результат, то l также безповторен.

LaTeX

$$$ \\operatorname{Nodup}(\\operatorname{map} f l) \\rightarrow \\operatorname{Nodup}(l) $$$

Lean4

theorem of_map (f : α → β) {l : List α} : Nodup (map f l) → Nodup l :=
  (Pairwise.of_map f) fun _ _ => mt <| congr_arg f

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

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

Разделы

Аффилиация

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