of_antisymmRel_of_compRel — Mathlib

English

If AntisymmRel (≤) a b holds and CompRel (≤) b c holds, then CompRel (≤) a c holds.

Русский

Если AntisymmRel (≤) a b выполняется и CompRel (≤) b c выполняется, тогда CompRel (≤) a c.

LaTeX

$$AntisymmRel(\le) a b \Rightarrow CompRel(\le) b c \Rightarrow CompRel(\le) a c$$

Lean4

@[trans]
theorem of_antisymmRel_of_compRel (h₁ : AntisymmRel (· ≤ ·) a b) (h₂ : CompRel (· ≤ ·) b c) : CompRel (· ≤ ·) a c :=
  (h₂.symm.trans_antisymmRel h₁.symm).symm

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