incompRel_of_antisymmRel_of_incompRel

English

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

Русский

Если AntisymmRel (≤) a b и IncompRel (≤) b c, то IncompRel (≤) a c.

LaTeX

$$AntisymmRel(≤) a b \rightarrow IncompRel(≤) b c \rightarrow IncompRel(≤) a c$$

Lean4

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

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