eq_lt — Mathlib

English

If o and a,b satisfy Compares o a b, then o = lt if and only if a < b.

Русский

Если o сравнивает a и b и выполняется Compares o a b, то o = lt тогда и только тогда, когда a < b.

LaTeX

$$$\\forall o\\ {a b},\\ Compares o a b \\rightarrow (o = \{lt\} \\leftrightarrow a < b)$$$

Lean4

theorem eq_lt [Preorder α] : ∀ {o} {a b : α}, Compares o a b → (o = lt ↔ a < b)
  | lt, _, _, h => ⟨fun _ => h, fun _ => rfl⟩
  | eq, a, b, h => ⟨fun h => by injection h, fun h' => (ne_of_lt h' h).elim⟩
  | gt, a, b, h => ⟨fun h => by injection h, fun h' => (lt_asymm h h').elim⟩

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