instTransCompRelLeAntisymmRel — Mathlib

English

There exists a transitive composition from AntisymmRel to CompRel to CompRel, defined by CompRel.of_antisymmRel_of_compRel.

Русский

Существует переходная связь между AntisymmRel и CompRel, определяемая CompRel.of_antisymmRel_of_compRel.

LaTeX

$$Trans( AntisymmRel(\le), CompRel(\le), CompRel(\le) )$$

Lean4

instance : @Trans α α α (CompRel (· ≤ ·)) (AntisymmRel (· ≤ ·)) (CompRel (· ≤ ·)) where
  trans := CompRel.of_compRel_of_antisymmRel

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