asymmetric₃ — Mathlib

English

Let r be a well-founded relation. If a, b, c are elements and r a b and r b c hold, then it is not the case that r c a.

Русский

Пусть r — хорошо основанное отношение. Для любых a, b, c из множества, если r a b и r b c, то не выполняется r c a.

LaTeX

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

Lean4

theorem asymmetric₃ {α : Sort*} {r : α → α → Prop} (h : WellFounded r) (a b c) : r a b → r b c → ¬r c a :=
  @WellFoundedRelation.asymmetric₃ _ ⟨_, h⟩ _ _
    _
      -- see Note [lower instance priority]

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