incompRel_congr_right — Mathlib

English

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

Русский

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

LaTeX

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

Lean4

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

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