sublist

Mathlib.Data.List.Sigma

URI: https://scilib.ai/kg/mathlib#List.NodupKeys.sublist

English

If l1 is a sublist of l2 and l2 has NodupKeys, then l1 has NodupKeys.

Русский

Если l1 является подсписком l2, и l2 имеет NodupKeys, то l1 имеет NodupKeys.

LaTeX

$$$ l_1\\ <+\\ l_2 \\implies l_2.NodupKeys \\Rightarrow l_1.NodupKeys $$$

Lean4

theorem sublist {l₁ l₂ : List (Sigma β)} (h : l₁ <+ l₂) : NodupKeys l₂ → NodupKeys l₁ :=
  Nodup.sublist <| h.map _

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

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

Разделы

Аффилиация

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