map

Mathlib.Data.List.Nodup

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

English

If f is injective, then Nodup(l) implies Nodup(map f l).

Русский

Если f инъективна, то из безповторности l следует безповторность map f l.

LaTeX

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

Lean4

protected theorem map {f : α → β} (hf : Injective f) : Nodup l → Nodup (map f l) :=
  Nodup.map_on fun _ _ _ _ h => hf h

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

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

Разделы

Аффилиация

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