lt_or_le_of_codirected — Mathlib

English

For r ≤ v1 and r ≤ v2 in a Preorder with SuccOrder and IsSuccArchimedean, either v1 < v2 or v2 ≤ v1.

Русский

При r ≤ v1 и r ≤ v2 в предордере с SuccOrder и IsSuccArchimedean имеет либо v1 < v2, либо v2 ≤ v1.

LaTeX

$$$v_1 < v_2 \lor v_2 \le v_1$ under the given hypotheses$$

Lean4

theorem lt_or_le_of_codirected [SuccOrder α] [IsSuccArchimedean α] {r v₁ v₂ : α} (h₁ : r ≤ v₁) (h₂ : r ≤ v₂) :
    v₁ < v₂ ∨ v₂ ≤ v₁ := by
  rw [Classical.or_iff_not_imp_right]
  intro nh
  rcases le_total_of_codirected h₁ h₂ with h | h
  · apply lt_of_le_of_ne h (ne_of_not_le nh).symm
  · contradiction

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