of_compRel_of_antisymmRel — Mathlib

English

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

Русский

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

LaTeX

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

Lean4

@[trans]
theorem of_compRel_of_antisymmRel (h₁ : CompRel (· ≤ ·) a b) (h₂ : AntisymmRel (· ≤ ·) b c) : CompRel (· ≤ ·) a c :=
  by
  obtain (h | h) := h₁
  · exact (h.trans h₂.le).compRel
  · exact (h₂.ge.trans h).compRel_symm

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