nontrivial_iff_exists_lt — Mathlib

English

For a LinearOrder α, a subset s is nontrivial if and only if there exist x ∈ s and y ∈ s with x < y.

Русский

Для линейного порядка α множество s не тривиально тогда и только тогда, когда существуют x ∈ s и y ∈ s такие, что x < y.

LaTeX

$$$s.Nontrivial \iff \exists x \in s, \exists y \in s, x < y$$$

Lean4

theorem nontrivial_iff_exists_lt [LinearOrder α] : s.Nontrivial ↔ ∃ᵉ (x ∈ s) (y ∈ s), x < y :=
  ⟨Nontrivial.exists_lt, nontrivial_of_exists_lt⟩

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