incompRel_congr_left — Mathlib

English

If a and b are related by antisymmetry of ≤, then IncompRel ≤ a c is equivalent to IncompRel ≤ b c for all c.

Русский

Если a и b связаны антисимметрией ≤, то для любого c несопоставимость a с c эквивалентна несопоставимости b с c.

LaTeX

$$$\\forall a\\ b\\ c, AntisymmRel(\\le) \\ a \\ b \\rightarrow IncompRel(\\le) \\ a \\ c \\leftrightarrow IncompRel(\\le) \\ b \\ c$$$

Lean4

theorem incompRel_congr_left (h : AntisymmRel (· ≤ ·) a b) : IncompRel (· ≤ ·) a c ↔ IncompRel (· ≤ ·) b c :=
  h.incompRel_congr AntisymmRel.rfl

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