prev_getLast_cons

Mathlib.Data.List.Cycle

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

Lean4

@[simp]
theorem prev_getLast_cons (h : x ∈ x :: l) : prev (x :: l) x h = getLast (x :: l) (cons_ne_nil _ _) :=
  prev_getLast_cons' l x x h rfl

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

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

Разделы

Аффилиация

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