lookupAll_nodup

Mathlib.Data.List.Sigma

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

← MathLib Explorer

English

If l has NodupKeys, then lookupAll a l is Nodup.

Русский

Если l имеет NodupKeys, то lookupAll a l является Nodup.

LaTeX

$$$ (\mathrm{lookupAll} a l).Nodup $$$

Lean4

theorem lookupAll_nodup (a : α) {l : List (Sigma β)} (h : l.NodupKeys) : (lookupAll a l).Nodup := by
  (rw [lookupAll_eq_dlookup a h]; apply Option.toList_nodup)

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

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

Разделы

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

Аффилиация

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