to_nonempty — Mathlib

English

Every nontrivial type has a nonempty instance.

Русский

Каждый не тривиальный тип имеет непустый элемент.

LaTeX

$$$[\text{Nontrivial}(\alpha)] \Rightarrow \text{Nonempty}(\alpha)$$$

Lean4

/-- See Note [lower instance priority]

Note that since this and `instNonemptyOfInhabited` are the most "obvious" way to find a nonempty
instance if no direct instance can be found, we give this a higher priority than the usual `100`.
-/
instance (priority := 500) to_nonempty [Nontrivial α] : Nonempty α :=
  let ⟨x, _⟩ := _root_.exists_pair_ne α
  ⟨x⟩

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