prev_cons_cons_of_ne'

Mathlib.Data.List.Cycle

URI: https://scilib.ai/kg/mathlib#List.prev_cons_cons_of_ne'

← MathLib Explorer

English

If x ∈ y :: z :: l and x ≠ y and x = z, then prev (y :: z :: l) x h = y.

Русский

Если x ∈ y :: z :: l, x ≠ y и x = z, то prev (y :: z :: l) x h = y.

LaTeX

$$$\\forall x\\in y::z::l,\\ x\\neq y,\\ x=z\\Rightarrow Prev(y::z::l)\\ x h = y$$$

Lean4

theorem prev_cons_cons_of_ne' (y z : α) (h : x ∈ y :: z :: l) (hy : x ≠ y) (hz : x = z) : prev (y :: z :: l) x h = y :=
  by
  cases l
  · simp [prev, hz]
  · rw [prev, dif_neg hy, if_pos hz]

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

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

Разделы

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

Аффилиация

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