insertIdx_subset_cons

Mathlib.Data.List.InsertIdx

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

← MathLib Explorer

English

The substituted list l.insertIdx n a is a subset of a :: l.

Русский

Список l.insertIdx n a является подмножеством a :: l.

LaTeX

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

Lean4

theorem insertIdx_subset_cons (n : ℕ) (a : α) (l : List α) : l.insertIdx n a ⊆ a :: l :=
  by
  intro b hb
  simpa using eq_or_mem_of_mem_insertIdx hb

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

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

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

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