exists_ne — Mathlib

English

If α is nonempty and equality is decidable, then for any x there exists y ≠ x.

Русский

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

LaTeX

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

Lean4

protected theorem exists_ne [Nontrivial α] [DecidableEq α] (x : α) : ∃ y, y ≠ x :=
  by
  rcases exists_pair_ne α with ⟨y, y', h⟩
  by_cases hx : x = y
  · rw [← hx] at h
    exact ⟨y', h.symm⟩
  · exact ⟨y, Ne.symm hx⟩

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