elim_singleton

Mathlib.Data.List.Duplicate

URI: https://scilib.ai/kg/mathlib#List.Duplicate.elim_singleton

English

No element can duplicate a singleton list [y].

Русский

Никакой элемент не может дублировать одиночный список [y].

LaTeX

$$$\forall \alpha\, \forall x:\alpha,\forall y:\alpha,\; x \in+ [y] \Rightarrow \text{False}$$$

Lean4

theorem elim_singleton {y : α} (h : x ∈+ [y]) : False :=
  not_duplicate_singleton x y h

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

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

Разделы

Аффилиация

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