get_attach

Mathlib.Data.List.Basic

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

English

The i-th element of l.attach equals the i-th element of l, by underlying indexing.

Русский

i-й элемент l.attach равен i-му элементу l, по базовым индексам.

LaTeX

$$$ \\forall i < |l|_\\text{attach},\\ (l.\\text{attach}.get i).1 = l.\\text{get} \\langle i, \\text{length\\_attach}(l) \\rangle $$$

Lean4

theorem get_attach (l : List α) (i) : (l.attach.get i).1 = l.get ⟨i, length_attach (l := l) ▸ i.2⟩ := by simp

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

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

Разделы

Аффилиация

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