toList_nodup

Mathlib.Data.List.Nodup

URI: https://scilib.ai/kg/mathlib#Option.toList_nodup

English

For every o in Option α, the toList image is a nodup list.

Русский

Для любого o ∈ Option α образ toList является списком без повторов.

LaTeX

$$$ \\forall o:\\\\mathrm{Option}(\\alpha), (o.{\\\\toList}).\\\\Nodup. $$$

Lean4

theorem toList_nodup : ∀ o : Option α, o.toList.Nodup
  | none => List.nodup_nil
  | some x => List.nodup_singleton x

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

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

Разделы

Аффилиация

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