sym_sublist_sym_cons

Mathlib.Data.List.Sym

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

English

For any xs, any n and any a, xs.sym n is a sublist of (a :: xs).sym n.

Русский

Для любого xs, любого n и любого элемента a, xs.sym n является подпоследовательностью (a :: xs).sym n.

LaTeX

$$$ (xs.sym n) \Subseteq (a :: xs).sym n $$$

Lean4

theorem sym_sublist_sym_cons {a : α} : xs.sym n <+ (a :: xs).sym n :=
  (sublist_cons_self a xs).sym n

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

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

Разделы

Аффилиация

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