English
Let α be a partially ordered set with PredOrder and IsPredArchimedean. For any r, v1, v2 ∈ α with v1 ≤ r and v2 ≤ r, we have either v1 < v2 or v2 ≤ v1.
Русский
Пусть α — частично упорядованный множество с PredOrder и IsPredArchimedean. Для любых r, v1, v2 ∈ α с выполнением v1 ≤ r и v2 ≤ r справедливо либо v1 < v2, либо v2 ≤ v1.
LaTeX
$$$ \forall \alpha \ [\text{PartialOrder }\alpha] \ [\text{PredOrder }\alpha] \ [\text{IsPredArchimedean }\alpha]\; {r, v_1, v_2 \in \alpha},\; v_1 \le r \land v_2 \le r \Rightarrow (v_1 < v_2) \lor (v_2 \le v_1).$$$
Lean4
theorem lt_or_le_of_directed [PredOrder α] [IsPredArchimedean α] {r v₁ v₂ : α} (h₁ : v₁ ≤ r) (h₂ : v₂ ≤ r) :
v₁ < v₂ ∨ v₂ ≤ v₁ := by
rw [Classical.or_iff_not_imp_right]
intro nh
rcases le_total_of_directed h₁ h₂ with h | h
· apply lt_of_le_of_ne h (ne_of_not_le nh).symm
· contradiction
