English
Let r be a relation on α that is asymmetric. Then for all a,b, if a is related to b by r, then b is not related to a by r.
Русский
Пусть r — отношение на α, удовлетворяющее свойству асимметрии. Тогда для любых a, b: если a ≺ b, то не b ≺ a.
LaTeX
$$$\forall a,b : \alpha, a \prec b \rightarrow \neg b \prec a$$$
Lean4
theorem asymm [IsAsymm α r] : a ≺ b → ¬b ≺ a :=
IsAsymm.asymm _ _