exists_ne

Mathlib.Logic.Nontrivial.Defs

URI: https://scilib.ai/kg/mathlib#exists_ne

English

If α is nontrivial, then for any x there exists y ≠ x.

Русский

Если тип не тривиален, то для любого элемента x существует y, отличный от x.

LaTeX

$$$[\text{Nontrivial}(\alpha)](x) \Rightarrow \exists y:\, \alpha, y \neq x$$$

Lean4

theorem exists_ne [Nontrivial α] (x : α) : ∃ y, y ≠ x :=
  Decidable.exists_ne x

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

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

Разделы

Аффилиация

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