nodup_attach

Mathlib.Data.List.Nodup

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

← MathLib Explorer

English

Nodup(attach l) holds if and only if Nodup(l).

Русский

Nodup(attach l) ⇔ Nodup(l).

LaTeX

$$$\\operatorname{Nodup}(\\mathrm{attach}(l)) \\iff \\operatorname{Nodup}(l)$$$

Lean4

@[simp]
theorem nodup_attach {l : List α} : Nodup (attach l) ↔ Nodup l :=
  ⟨fun h => attach_map_subtype_val l ▸ h.map fun _ _ => Subtype.eq, fun h =>
    Nodup.of_map Subtype.val ((attach_map_subtype_val l).symm ▸ h)⟩

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

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

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

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