doubleton_eq

Mathlib.Data.List.Basic

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

← MathLib Explorer

English

For distinct x,y, the two-element list {x,y} equals [x,y].

Русский

Для различных x и y двучленный список {x,y} равен [x,y].

LaTeX

$$x ≠ y → ({ x, y } : List α) = [x, y]$$

Lean4

theorem doubleton_eq [DecidableEq α] {x y : α} (h : x ≠ y) : ({ x, y } : List α) = [x, y] :=
  by
  rw [insert_neg, singleton_eq]
  rwa [singleton_eq, mem_singleton]

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

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

Разделы

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

Аффилиация

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