asymmetric — Mathlib

English

Every well-founded relation is asymmetric.

Русский

Каждое хорошо основанное отношение асимметрично.

LaTeX

$$$\\forall {\\alpha} {r}, [IsWellFounded r] \\Rightarrow (\\forall a,b, r a b \\rightarrow \\lnot r b a)$$$

Lean4

theorem asymmetric {α : Sort*} [WellFoundedRelation α] {a b : α} :
    WellFoundedRelation.rel a b → ¬WellFoundedRelation.rel b a := fun hab hba => WellFoundedRelation.asymmetric hba hab
termination_by a

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