inj — Mathlib

English

If two orderings o1 and o2 both compare a given pair a,b, then o1 = o2.

Русский

Если две характеристики порядка o1 и o2 дают одинаковое сравнение a и b, то o1 = o2.

LaTeX

$$$\\forall a\\ b,\\ Compares o1 a b \\rightarrow Compares o2 a b \\rightarrow o1 = o2$$$

Lean4

theorem inj [Preorder α] {o₁} : ∀ {o₂} {a b : α}, Compares o₁ a b → Compares o₂ a b → o₁ = o₂
  | lt, _, _, h₁, h₂ => h₁.eq_lt.2 h₂
  | eq, _, _, h₁, h₂ => h₁.eq_eq.2 h₂
  | gt, _, _, h₁, h₂ => h₁.eq_gt.2 h₂

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