instTransAntisymmRelLeIncompRel — Mathlib

English

Let α be a preorder. If a and b are related by antisymmetry of ≤, and b is incomparable with c with respect to ≤, then a is incomparable with c with respect to ≤.

Русский

Пусть α — частично упорядоченное множество. Пусть a и b связаны антисимметричностью отношения ≤, и b несопоставим с c по отношению ≤; тогда и a несопоставим с c по отношению ≤.

LaTeX

$$$\\forall a\\, b\\, c\\, AntisymmRel(\\le) \\ a \\ b \\rightarrow IncompRel(\\le) \\ b \\ c \\rightarrow IncompRel(\\le) \\ a \\ c$$$

Lean4

instance : @Trans α α α (AntisymmRel (· ≤ ·)) (IncompRel (· ≤ ·)) (IncompRel (· ≤ ·)) where
  trans := incompRel_of_antisymmRel_of_incompRel

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