nodup_map_iff

Mathlib.Data.List.Nodup

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

English

For injective f, Nodup(map f l) is equivalent to Nodup(l).

Русский

При инъективном f Nodup(map f l) эквивалентно Nodup(l).

LaTeX

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

Lean4

theorem nodup_map_iff {f : α → β} {l : List α} (hf : Injective f) : Nodup (map f l) ↔ Nodup l :=
  ⟨Nodup.of_map _, Nodup.map hf⟩

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

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

Разделы

Аффилиация

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