exists_lt — Mathlib

English

Let α be a LinearOrder and s a set. If s is nontrivial, then there exist x ∈ s and y ∈ s with x < y.

Русский

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

LaTeX

$$$\exists x \in s\, \exists y \in s, x < y$$$

Lean4

theorem exists_lt [LinearOrder α] (hs : s.Nontrivial) : ∃ᵉ (x ∈ s) (y ∈ s), x < y :=
  let ⟨x, hx, y, hy, hxy⟩ := hs
  Or.elim (lt_or_gt_of_ne hxy) (fun H => ⟨x, hx, y, hy, H⟩) fun H => ⟨y, hy, x, hx, H⟩

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