nontrivial_of_lt — Mathlib

English

From x < y in a preordered set, the order has two distinct elements, so the type is nontrivial.

Русский

Если существует x < y в предмножествах с порядком, то множество непродуктно с двумя различными элементами.

LaTeX

$$$\forall {\alpha} [\text{Preorder } \alpha], \; x,y : \alpha \;\to\; x < y \Rightarrow \operatorname{Nontrivial} \alpha$$$

Lean4

theorem nontrivial_of_lt [Preorder α] (x y : α) (h : x < y) : Nontrivial α :=
  ⟨⟨x, y, ne_of_lt h⟩⟩

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