subset_insertIdx

Mathlib.Data.List.InsertIdx

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

English

l is a subset of l.insertIdx n a.

Русский

l ⊆ l.insertIdx n a.

LaTeX

$$$l \\subseteq l.insertIdx n a$$$

Lean4

@[simp]
theorem subset_insertIdx (l : List α) (n : ℕ) (a : α) : l ⊆ l.insertIdx n a :=
  (sublist_insertIdx ..).subset

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

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

Разделы

Аффилиация

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