nodup_zipIdx_map_snd

Mathlib.Data.List.Sigma

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

English

For any list l, the list of second components of l.zipIdx, after mapping by Prod.snd, is nodup.

Русский

Для любого списка l, список вторых компонент после применения zipIdx и маппинга Prod.snd пусто повторений.

LaTeX

$$$ (l.zipIdx.map\\, Prod.snd).Nodup $$$

Lean4

theorem nodup_zipIdx_map_snd (l : List α) : (l.zipIdx.map Prod.snd).Nodup := by simp [List.nodup_range']

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

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

Разделы

Аффилиация

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