incompRel_of_incompRel_of_antisymmRel

English

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

Русский

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

LaTeX

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

Lean4

@[trans]
theorem incompRel_of_incompRel_of_antisymmRel (h₁ : IncompRel (· ≤ ·) a b) (h₂ : AntisymmRel (· ≤ ·) b c) :
    IncompRel (· ≤ ·) a c :=
  ⟨fun h ↦ h₁.not_le (h.trans h₂.ge), fun h ↦ h₁.not_ge (h₂.le.trans h)⟩

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