of_append_right

Mathlib.Data.List.Nodup

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

English

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

Русский

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

LaTeX

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

Lean4

theorem of_append_right : Nodup (l₁ ++ l₂) → Nodup l₂ :=
  Nodup.sublist (sublist_append_right l₁ l₂)

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

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

Разделы

Аффилиация

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