to_nontrivial — Mathlib

English

Let α be a type equipped with a two-pointing p. Then α is nontrivial; equivalently, there exist a,b ∈ α with a ≠ b (for instance a = p.fst and b = p.snd).

Русский

Пусть α — тип, имеющий два специально выделенных элемента; тогда α не тривиален; то есть существуют a,b ∈ α такие, что a ≠ b (например a = p.fst и b = p.snd).

LaTeX

$$$\\exists a,b: \\alpha, a \\neq b$$$

Lean4

theorem to_nontrivial : Nontrivial α :=
  ⟨⟨p.fst, p.snd, p.fst_ne_snd⟩⟩

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