English
For a linear order, either there is an element strictly between a₁ and a₂, or the pair (a₁,a₂) is dense-discrete in the sense that all elements lie on one side: a₁ < a → a₂ ≤ a or a < a₂ → a ≤ a₁.
Русский
Для линейного порядка либо существует элемент между a₁ и a₂, либо пара (a₁,a₂) распределена так, что все элементы лежат по одну сторону: a₁ < a → a₂ ≤ a и т. д.
LaTeX
$$∃ a, a₁ < a ∧ a < a₂ ∨ (∀ a, a₁ < a → a₂ ≤ a) ∧ ∀ a < a₂, a ≤ a₁$$
Lean4
theorem dense_or_discrete [LinearOrder α] (a₁ a₂ : α) :
(∃ a, a₁ < a ∧ a < a₂) ∨ (∀ a, a₁ < a → a₂ ≤ a) ∧ ∀ a < a₂, a ≤ a₁ :=
or_iff_not_imp_left.2 fun h ↦
⟨fun a ha₁ ↦ le_of_not_gt fun ha₂ ↦ h ⟨a, ha₁, ha₂⟩, fun a ha₂ ↦ le_of_not_gt fun ha₁ ↦ h ⟨a, ha₁, ha₂⟩⟩
