instIsAsymmRel — Mathlib

English

If α has a well-founded relation, then the corresponding WellFoundedRelation.rel is asymmetric.

Русский

Если у множества есть хорошо основанное отношение, то соответствующее отношение WellFoundedRelation.rel асимметрично.

LaTeX

$$$IsAsymm\ α\ WellFoundedRelation.rel$$$

Lean4

instance [WellFoundedRelation α] : IsAsymm α WellFoundedRelation.rel :=
  WellFoundedRelation.wf.isAsymm

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