antisymm_of' — Mathlib

English

A variant of antisymmetry with explicit relation: r a b → r b a → b = a.

Русский

Вариант антисимметрии с явным отношением: r a b → r b a → b = a.

LaTeX

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

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 → b = a :=
  antisymm'

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