English
If a linear order has no triple x < y < z, then for any x,y,z one has x = y or y = z or x = z (at most two distinct elements).
Русский
Если в линейном порядке нет тройки x < y < z, то любые три элемента содержат хотя бы две равные; то есть максимум два различных элемента.
LaTeX
$$$x = y \lor y = z \lor x = z$$$
Lean4
/-- If a linear order has no elements `x < y < z`, then it has at most two elements. -/
theorem eq_or_eq_or_eq_of_forall_not_lt_lt [LinearOrder α] (h : ∀ ⦃x y z : α⦄, x < y → y < z → False) (x y z : α) :
x = y ∨ y = z ∨ x = z := by
by_contra hne
simp only [not_or, ← Ne.eq_def] at hne
rcases hne.1.lt_or_gt with h₁ | h₁ <;> rcases hne.2.1.lt_or_gt with h₂ | h₂ <;> rcases hne.2.2.lt_or_gt with h₃ | h₃
exacts [h h₁ h₂, h h₂ h₃, h h₃ h₂, h h₃ h₁, h h₁ h₃, h h₂ h₃, h h₁ h₃, h h₂ h₁]
