le_antisymm — Mathlib

English

If o a b is satisfied and a ≤ b and b ≤ a, then a = b.

Русский

Если o удовлетворяет условию compares a b и a ≤ b и b ≤ a, то a = b.

LaTeX

$$$\\forall a\\ b,\\ Compares o a b \\rightarrow a \\le b \\rightarrow b \\le a \\rightarrow a = b$$$

Lean4

theorem le_antisymm [Preorder α] {a b : α} : ∀ {o}, Compares o a b → a ≤ b → b ≤ a → a = b
  | lt, h, _, hba => (not_le_of_gt h hba).elim
  | eq, h, _, _ => h
  | gt, h, hab, _ => (not_le_of_gt h hab).elim

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