eq_eq — Mathlib

English

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

Русский

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

LaTeX

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

Lean4

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

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