nontrivial_iff_lt — Mathlib

English

A linear order is nontrivial iff there exist x ≠ y with x < y.

Русский

Линейный порядок не тривиален тогда и только тогда, когда существуют x ≠ y с x < y.

LaTeX

$$$\forall {\alpha} [\text{LinearOrder } \alpha], \; \operatorname{Nontrivial} \alpha \iff \exists x \exists y, x < y$$$

Lean4

theorem nontrivial_iff_lt [LinearOrder α] : Nontrivial α ↔ ∃ x y : α, x < y :=
  ⟨fun h ↦ @exists_pair_lt α h _, fun ⟨x, y, h⟩ ↦ nontrivial_of_lt x y h⟩

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