asymm — Mathlib

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 _ _

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