ne_lt — Mathlib

English

If o and a,b satisfy Compares o a b, then o ≠ lt if and only if b ≤ a.

Русский

Если o сравнивает a и b, то o ≠ lt тогда и только тогда, когда b ≤ a.

LaTeX

$$$\\forall o\\ {a b},\\ Compares o a b \\rightarrow (o \\neq lt \\leftrightarrow b \\le a)$$$

Lean4

theorem ne_lt [Preorder α] : ∀ {o} {a b : α}, Compares o a b → (o ≠ lt ↔ b ≤ a)
  | lt, _, _, h => ⟨absurd rfl, fun h' => (not_le_of_gt h h').elim⟩
  | eq, _, _, h => ⟨fun _ => ge_of_eq h, fun _ h => by injection h⟩
  | gt, _, _, h => ⟨fun _ => le_of_lt h, fun _ h => by injection h⟩

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