subperm_cons_self

Mathlib.Data.List.Perm.Subperm

URI: https://scilib.ai/kg/mathlib#List.subperm_cons_self

English

For any list l and element a, l is a subpermutation of a :: l.

Русский

Для любого списка l и элемента a, l — подпермутация к списку a :: l.

LaTeX

$$$l <+~ a :: l$$$

Lean4

theorem subperm_cons_self : l <+~ a :: l :=
  ⟨l, Perm.refl _, sublist_cons_self _ _⟩

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

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

Разделы

Аффилиация

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