of_append_left

Mathlib.Data.List.Nodup

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

English

If the concatenation l1 ++ l2 is nodup, then l1 is nodup.

Русский

Если конкатенация l1 ++ l2 состоит из без повторов, то и l1 состоит из без повторов.

LaTeX

$$$ \\operatorname{Nodup}(l_1 ++ l_2) \\rightarrow \\operatorname{Nodup}(l_1) $$$

Lean4

theorem of_append_left : Nodup (l₁ ++ l₂) → Nodup l₁ :=
  Nodup.sublist (sublist_append_left l₁ l₂)

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

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

Разделы

Аффилиация

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