instIsAsymmOfIsWellFounded — Mathlib

English

If r is a well-founded relation, then r is asymmetric: for all a,b, r a b implies not r b a.

Русский

Если r — хорошо основанное отношение, то оно асимметрично: для любых a,b верно, что r a b приводит к не r b a.

LaTeX

$$$\\mathrm{WellFounded}(r) \\rightarrow \\forall a,b,\\ r\\ a\\ b \\rightarrow \\neg r\\ b\\ a$$$

Lean4

instance (priority := 100) (r : α → α → Prop) [IsWellFounded α r] : IsAsymm α r :=
  ⟨IsWellFounded.wf.asymmetric⟩
    -- see Note [lower instance priority]

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