antisymm_of — Mathlib

English

If r is antisymmetric, then r a b → r b a → a = b.

Русский

Если r антисимметрично, то r a b и r b a ⇒ a = b.

LaTeX

$$$\\\\forall {a,b}, \\\\ r(a,b) \\\\rightarrow \\\\ r(b,a) \\\\rightarrow a = b.$$$

Lean4

/-- A version of `antisymm` with `r` explicit.

This lemma matches the lemmas from lean core in `Init.Algebra.Classes`, but is missing there. -/
@[elab_without_expected_type]
theorem antisymm_of (r : α → α → Prop) [IsAntisymm α r] {a b : α} : r a b → r b a → a = b :=
  antisymm

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