subperm

Mathlib.Data.List.Perm.Subperm

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

English

If l1 is noduplicate and l1 is a subset of l2, then l1 is a subpermutation of l2.

Русский

Если l1 без повторов и l1 ⊆ l2, то l1 является подпермутацией к l2.

LaTeX

$$$l_1.Nodup \land l_1 \subseteq l_2 \Rightarrow l_1 <+~ l_2$$$

Lean4

protected theorem subperm (d : Nodup l₁) (H : l₁ ⊆ l₂) : l₁ <+~ l₂ :=
  subperm_of_subset d H

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

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

Разделы

Аффилиация

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